{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE RecordWildCards            #-}
{-# LANGUAGE ConstraintKinds            #-}
{-# LANGUAGE DerivingVia                #-}
{-# LANGUAGE NamedFieldPuns             #-}
{-# LANGUAGE TupleSections              #-}
{-# LANGUAGE TypeOperators              #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE ScopedTypeVariables        #-}

{-# OPTIONS_GHC -Wno-orphans #-}

-- | This module should contain all the global type definitions and basic instances.

module Language.Haskell.Liquid.Types.RTypeOp (

  -- * Constructing & Destructing RTypes
    SpecRep
  , RTypeRep, RTypeRepV, RTypeRepBV(..), fromRTypeRep, toRTypeRep
  , mkArrow, bkArrowDeep, bkArrow, safeBkArrow
  , mkUnivs, bkUniv, bkClass, bkUnivClass, bkUnivClass'
  , rFun, rFun', rCls, rRCls, rFunDebug
  , classRFInfoType

  -- * Traversing `RType`
  , efoldReft, foldReft, foldReft'
  , emapReft, mapReft, mapReftM, mapPropM
  , emapReftM, emapRefM
  , mapExprReft
  , mapBot, mapBind, mapRFInfo
  , foldRType
  , emapFReftM
  , mapRTypeV
  , mapRTypeVM
  , mapDataDeclV
  , mapDataDeclVM
  , emapDataDeclM
  , emapDataCtorTyM
  , emapBareTypeVM
  , parsedToBareType

  -- * Converting To and From Sort
  , ofRSort, toRSort
  , rTypeValueVar
  , rTypeReft
  , stripRTypeBase
  , topRTypeBase

  -- * Some tests on RTypes
  , isBase
  , isFunTy
  , isTrivial
  , hasHoleTy

  -- * Scoping Info
  , BScope

  -- * Misc
  , addInvCond
  , insertsSEnv
  )
  where

import qualified Liquid.GHC.API as Ghc
import           Prelude                          hiding  (error)
import qualified Prelude

import           Control.Monad                          (liftM2, liftM3, liftM4)
import           Data.Bifunctor (bimap)
import           Data.Hashable (Hashable)

import qualified Language.Fixpoint.Types as F
import           Language.Fixpoint.Types (ExprBV, Symbol)

import           Language.Haskell.Liquid.Types.DataDecl
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.Names
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Misc


-----------------------------------------------------------------------------
-- | Information about scope Binders Scope in
-----------------------------------------------------------------------------
{- In types with base refinement, e.g., {out:T {inner:a | ri} | ro }
If BScope = True , then the outer binder out is     in scope on ri
If BScope = False, then the outer binder out is not in scope on ri
-}

type BScope = Bool

--------------------------------------------------------------------------------
-- | Constructor and Destructors for RTypes ------------------------------------
--------------------------------------------------------------------------------
type RRep        = RTypeRep RTyCon RTyVar
type SpecRep     = RRep      RReft

type RTypeRep = RTypeRepV Symbol
type RTypeRepV = RTypeRepBV Symbol
data RTypeRepBV b v c tv r = RTypeRep
  { forall b v c tv r.
RTypeRepBV b v c tv r
-> [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
ty_vars   :: [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
  , forall b v c tv r.
RTypeRepBV b v c tv r
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
ty_preds  :: [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
  , forall b v c tv r. RTypeRepBV b v c tv r -> [b]
ty_binds  :: [b]
  , forall b v c tv r. RTypeRepBV b v c tv r -> [RFInfo]
ty_info   :: [RFInfo]
  , forall b v c tv r. RTypeRepBV b v c tv r -> [r]
ty_refts  :: [r]
  , forall b v c tv r. RTypeRepBV b v c tv r -> [RTypeBV b v c tv r]
ty_args   :: [RTypeBV b v c tv r]
  , forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
ty_res    :: RTypeBV b v c tv r
  }

fromRTypeRep :: RTypeRepBV b v c tv r -> RTypeBV b v c tv r
fromRTypeRep :: forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
fromRTypeRep RTypeRep{[b]
[r]
[(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
[RTypeBV b v c tv r]
[PVarBV b v (RTypeBV b v c tv (NoReftB b))]
[RFInfo]
RTypeBV b v c tv r
ty_vars :: forall b v c tv r.
RTypeRepBV b v c tv r
-> [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
ty_preds :: forall b v c tv r.
RTypeRepBV b v c tv r
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
ty_binds :: forall b v c tv r. RTypeRepBV b v c tv r -> [b]
ty_info :: forall b v c tv r. RTypeRepBV b v c tv r -> [RFInfo]
ty_refts :: forall b v c tv r. RTypeRepBV b v c tv r -> [r]
ty_args :: forall b v c tv r. RTypeRepBV b v c tv r -> [RTypeBV b v c tv r]
ty_res :: forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
ty_vars :: [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
ty_preds :: [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
ty_binds :: [b]
ty_info :: [RFInfo]
ty_refts :: [r]
ty_args :: [RTypeBV b v c tv r]
ty_res :: RTypeBV b v c tv r
..}
  = [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
-> [(b, RFInfo, RTypeBV b v c tv r, r)]
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
forall tv b v c r.
[(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
-> [(b, RFInfo, RTypeBV b v c tv r, r)]
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
mkArrow [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
ty_vars [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
ty_preds [(b, RFInfo, RTypeBV b v c tv r, r)]
arrs RTypeBV b v c tv r
ty_res
  where
    arrs :: [(b, RFInfo, RTypeBV b v c tv r, r)]
arrs = [Char]
-> [b]
-> [RFInfo]
-> [RTypeBV b v c tv r]
-> [r]
-> [(b, RFInfo, RTypeBV b v c tv r, r)]
forall t1 t2 t3 t4.
[Char] -> [t1] -> [t2] -> [t3] -> [t4] -> [(t1, t2, t3, t4)]
safeZip4WithError ([Char]
"fromRTypeRep: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Int, Int, Int, Int) -> [Char]
forall a. Show a => a -> [Char]
show ([b] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [b]
ty_binds, [RFInfo] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RFInfo]
ty_info, [RTypeBV b v c tv r] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RTypeBV b v c tv r]
ty_args, [r] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [r]
ty_refts)) [b]
ty_binds [RFInfo]
ty_info [RTypeBV b v c tv r]
ty_args [r]
ty_refts

classRFInfoType :: Bool -> RType c tv r -> RType c tv r
classRFInfoType :: forall c tv r. Bool -> RType c tv r -> RType c tv r
classRFInfoType Bool
b = RTypeRepBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
fromRTypeRep (RTypeRepBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r)
-> (RTypeBV Symbol Symbol c tv r
    -> RTypeRepBV Symbol Symbol c tv r)
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                    (\trep :: RTypeRepBV Symbol Symbol c tv r
trep@RTypeRep{[r]
[(RTVar tv (RTypeBV Symbol Symbol c tv (NoReftB Symbol)), r)]
[Symbol]
[RTypeBV Symbol Symbol c tv r]
[PVarBV
   Symbol Symbol (RTypeBV Symbol Symbol c tv (NoReftB Symbol))]
[RFInfo]
RTypeBV Symbol Symbol c tv r
ty_vars :: forall b v c tv r.
RTypeRepBV b v c tv r
-> [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
ty_preds :: forall b v c tv r.
RTypeRepBV b v c tv r
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
ty_binds :: forall b v c tv r. RTypeRepBV b v c tv r -> [b]
ty_info :: forall b v c tv r. RTypeRepBV b v c tv r -> [RFInfo]
ty_refts :: forall b v c tv r. RTypeRepBV b v c tv r -> [r]
ty_args :: forall b v c tv r. RTypeRepBV b v c tv r -> [RTypeBV b v c tv r]
ty_res :: forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
ty_vars :: [(RTVar tv (RTypeBV Symbol Symbol c tv (NoReftB Symbol)), r)]
ty_preds :: [PVarBV
   Symbol Symbol (RTypeBV Symbol Symbol c tv (NoReftB Symbol))]
ty_binds :: [Symbol]
ty_info :: [RFInfo]
ty_refts :: [r]
ty_args :: [RTypeBV Symbol Symbol c tv r]
ty_res :: RTypeBV Symbol Symbol c tv r
..} -> RTypeRepBV Symbol Symbol c tv r
trep{ty_info = map (\RFInfo
i -> RFInfo
i{permitTC = pure b}) ty_info}) (RTypeRepBV Symbol Symbol c tv r
 -> RTypeRepBV Symbol Symbol c tv r)
-> (RTypeBV Symbol Symbol c tv r
    -> RTypeRepBV Symbol Symbol c tv r)
-> RTypeBV Symbol Symbol c tv r
-> RTypeRepBV Symbol Symbol c tv r
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                    RTypeBV Symbol Symbol c tv r -> RTypeRepBV Symbol Symbol c tv r
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep

--------------------------------------------------------------------------------
toRTypeRep           :: RTypeBV b v c tv r -> RTypeRepBV b v c tv r
--------------------------------------------------------------------------------
toRTypeRep :: forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep RTypeBV b v c tv r
t         = [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
-> [b]
-> [RFInfo]
-> [r]
-> [RTypeBV b v c tv r]
-> RTypeBV b v c tv r
-> RTypeRepBV b v c tv r
forall b v c tv r.
[(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
-> [b]
-> [RFInfo]
-> [r]
-> [RTypeBV b v c tv r]
-> RTypeBV b v c tv r
-> RTypeRepBV b v c tv r
RTypeRep [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
αs [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
πs [b]
xs [RFInfo]
is [r]
rs [RTypeBV b v c tv r]
ts RTypeBV b v c tv r
t''
  where
    ([(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
αs, [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
πs, RTypeBV b v c tv r
t') = RTypeBV b v c tv r
-> ([(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)],
    [PVarBV b v (RTypeBV b v c tv (NoReftB b))], RTypeBV b v c tv r)
forall b v tv c r.
RTypeBV b v tv c r
-> ([(RTVar c (RTypeBV b v tv c (NoReftB b)), r)],
    [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r)
bkUniv RTypeBV b v c tv r
t
    (([b]
xs, [RFInfo]
is, [RTypeBV b v c tv r]
ts, [r]
rs), RTypeBV b v c tv r
t'') = RTypeBV b v c tv r
-> (([b], [RFInfo], [RTypeBV b v c tv r], [r]), RTypeBV b v c tv r)
forall b v t t1 a.
RTypeBV b v t t1 a
-> (([b], [RFInfo], [RTypeBV b v t t1 a], [a]), RTypeBV b v t t1 a)
bkArrow RTypeBV b v c tv r
t'

mkArrow :: [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
        -> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
        -> [(b, RFInfo, RTypeBV b v c tv r, r)]
        -> RTypeBV b v c tv r
        -> RTypeBV b v c tv r
mkArrow :: forall tv b v c r.
[(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
-> [(b, RFInfo, RTypeBV b v c tv r, r)]
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
mkArrow [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
αs [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
πs [(b, RFInfo, RTypeBV b v c tv r, r)]
zts = [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
forall (t :: * -> *) (t1 :: * -> *) tv b v c r.
(Foldable t, Foldable t1) =>
t (RTVar tv (RTypeBV b v c tv (NoReftB b)), r)
-> t1 (PVarBV b v (RTypeBV b v c tv (NoReftB b)))
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
mkUnivs [(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
αs [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
πs (RTypeBV b v c tv r -> RTypeBV b v c tv r)
-> (RTypeBV b v c tv r -> RTypeBV b v c tv r)
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(b, RFInfo, RTypeBV b v c tv r, r)]
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
forall {t :: * -> *} {b} {v} {c} {tv} {r}.
Foldable t =>
t (b, RFInfo, RTypeBV b v c tv r, r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
mkRFuns [(b, RFInfo, RTypeBV b v c tv r, r)]
zts
  where
    mkRFuns :: t (b, RFInfo, RTypeBV b v c tv r, r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
mkRFuns t (b, RFInfo, RTypeBV b v c tv r, r)
xts RTypeBV b v c tv r
t = ((b, RFInfo, RTypeBV b v c tv r, r)
 -> RTypeBV b v c tv r -> RTypeBV b v c tv r)
-> RTypeBV b v c tv r
-> t (b, RFInfo, RTypeBV b v c tv r, r)
-> RTypeBV b v c tv r
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(b
b,RFInfo
i,RTypeBV b v c tv r
t1,r
r) RTypeBV b v c tv r
t2 -> b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
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 b
b RFInfo
i RTypeBV b v c tv r
t1 RTypeBV b v c tv r
t2 r
r) RTypeBV b v c tv r
t t (b, RFInfo, RTypeBV b v c tv r, r)
xts

-- Do I need to keep track of implicits here too?
bkArrowDeep :: RType t t1 a -> ([Symbol], [RFInfo], [RType t t1 a], [a], RType t t1 a)
bkArrowDeep :: forall t t1 a.
RType t t1 a
-> ([Symbol], [RFInfo], [RType t t1 a], [a], RType t t1 a)
bkArrowDeep (RAllT RTVUBV Symbol Symbol t t1
_ RTypeBV Symbol Symbol t t1 a
t a
_)   = RTypeBV Symbol Symbol t t1 a
-> ([Symbol], [RFInfo], [RTypeBV Symbol Symbol t t1 a], [a],
    RTypeBV Symbol Symbol t t1 a)
forall t t1 a.
RType t t1 a
-> ([Symbol], [RFInfo], [RType t t1 a], [a], RType t t1 a)
bkArrowDeep RTypeBV Symbol Symbol t t1 a
t
bkArrowDeep (RAllP PVUBV Symbol Symbol t t1
_ RTypeBV Symbol Symbol t t1 a
t)     = RTypeBV Symbol Symbol t t1 a
-> ([Symbol], [RFInfo], [RTypeBV Symbol Symbol t t1 a], [a],
    RTypeBV Symbol Symbol t t1 a)
forall t t1 a.
RType t t1 a
-> ([Symbol], [RFInfo], [RType t t1 a], [a], RType t t1 a)
bkArrowDeep RTypeBV Symbol Symbol t t1 a
t
bkArrowDeep (RFun Symbol
x RFInfo
i RTypeBV Symbol Symbol t t1 a
t RTypeBV Symbol Symbol t t1 a
t' a
r) = let ([Symbol]
xs, [RFInfo]
is, [RTypeBV Symbol Symbol t t1 a]
ts, [a]
rs, RTypeBV Symbol Symbol t t1 a
t'') = RTypeBV Symbol Symbol t t1 a
-> ([Symbol], [RFInfo], [RTypeBV Symbol Symbol t t1 a], [a],
    RTypeBV Symbol Symbol t t1 a)
forall t t1 a.
RType t t1 a
-> ([Symbol], [RFInfo], [RType t t1 a], [a], RType t t1 a)
bkArrowDeep RTypeBV Symbol Symbol t t1 a
t' in
                                (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
xs, RFInfo
iRFInfo -> [RFInfo] -> [RFInfo]
forall a. a -> [a] -> [a]
:[RFInfo]
is, RTypeBV Symbol Symbol t t1 a
tRTypeBV Symbol Symbol t t1 a
-> [RTypeBV Symbol Symbol t t1 a] -> [RTypeBV Symbol Symbol t t1 a]
forall a. a -> [a] -> [a]
:[RTypeBV Symbol Symbol t t1 a]
ts, a
ra -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
rs, RTypeBV Symbol Symbol t t1 a
t'')
bkArrowDeep RTypeBV Symbol Symbol t t1 a
t               = ([], [], [], [], RTypeBV Symbol Symbol t t1 a
t)

bkArrow :: RTypeBV b v t t1 a -> ( ([b], [RFInfo], [RTypeBV b v t t1 a], [a])
                                 , RTypeBV b v t t1 a )
bkArrow :: forall b v t t1 a.
RTypeBV b v t t1 a
-> (([b], [RFInfo], [RTypeBV b v t t1 a], [a]), RTypeBV b v t t1 a)
bkArrow RTypeBV b v t t1 a
t                = (([b]
xs,[RFInfo]
is,[RTypeBV b v t t1 a]
ts,[a]
rs),RTypeBV b v t t1 a
t')
  where
    ([b]
xs, [RFInfo]
is, [RTypeBV b v t t1 a]
ts, [a]
rs, RTypeBV b v t t1 a
t') = RTypeBV b v t t1 a
-> ([b], [RFInfo], [RTypeBV b v t t1 a], [a], RTypeBV b v t t1 a)
forall b v t t1 a.
RTypeBV b v t t1 a
-> ([b], [RFInfo], [RTypeBV b v t t1 a], [a], RTypeBV b v t t1 a)
bkFun RTypeBV b v t t1 a
t

bkFun :: RTypeBV b v t t1 a -> ([b], [RFInfo], [RTypeBV b v t t1 a], [a], RTypeBV b v t t1 a)
bkFun :: forall b v t t1 a.
RTypeBV b v t t1 a
-> ([b], [RFInfo], [RTypeBV b v t t1 a], [a], RTypeBV b v t t1 a)
bkFun (RFun b
x RFInfo
i RTypeBV b v t t1 a
t RTypeBV b v t t1 a
t' a
r) = let ([b]
xs, [RFInfo]
is, [RTypeBV b v t t1 a]
ts, [a]
rs, RTypeBV b v t t1 a
t'') = RTypeBV b v t t1 a
-> ([b], [RFInfo], [RTypeBV b v t t1 a], [a], RTypeBV b v t t1 a)
forall b v t t1 a.
RTypeBV b v t t1 a
-> ([b], [RFInfo], [RTypeBV b v t t1 a], [a], RTypeBV b v t t1 a)
bkFun RTypeBV b v t t1 a
t' in
                          (b
xb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
xs, RFInfo
iRFInfo -> [RFInfo] -> [RFInfo]
forall a. a -> [a] -> [a]
:[RFInfo]
is, RTypeBV b v t t1 a
tRTypeBV b v t t1 a -> [RTypeBV b v t t1 a] -> [RTypeBV b v t t1 a]
forall a. a -> [a] -> [a]
:[RTypeBV b v t t1 a]
ts, a
ra -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
rs, RTypeBV b v t t1 a
t'')
bkFun RTypeBV b v t t1 a
t                 = ([], [], [], [], RTypeBV b v t t1 a
t)

safeBkArrow ::(F.PPrint (RType t t1 a))
            => RType t t1 a -> ( ([Symbol], [RFInfo], [RType t t1 a], [a])
                               , RType t t1 a )
safeBkArrow :: forall t t1 a.
PPrint (RType t t1 a) =>
RType t t1 a
-> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType t t1 a)
safeBkArrow t :: RType t t1 a
t@RAllT {} = [Char] -> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType t t1 a)
forall a. HasCallStack => [Char] -> a
Prelude.error {- panic Nothing -} ([Char]
 -> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType t t1 a))
-> [Char]
-> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType t t1 a)
forall a b. (a -> b) -> a -> b
$ [Char]
"safeBkArrow on RAllT" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ RType t t1 a -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp RType t t1 a
t
safeBkArrow (RAllP PVUBV Symbol Symbol t t1
_ RType t t1 a
_)     = [Char] -> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType t t1 a)
forall a. HasCallStack => [Char] -> a
Prelude.error {- panic Nothing -} [Char]
"safeBkArrow on RAllP"
safeBkArrow RType t t1 a
t               = RType t t1 a
-> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType t t1 a)
forall b v t t1 a.
RTypeBV b v t t1 a
-> (([b], [RFInfo], [RTypeBV b v t t1 a], [a]), RTypeBV b v t t1 a)
bkArrow RType t t1 a
t

mkUnivs :: (Foldable t, Foldable t1)
        => t  (RTVar tv (RTypeBV b v c tv (NoReftB b)), r)
        -> t1 (PVarBV b v (RTypeBV b v c tv (NoReftB b)))
        -> RTypeBV b v c tv r
        -> RTypeBV b v c tv r
mkUnivs :: forall (t :: * -> *) (t1 :: * -> *) tv b v c r.
(Foldable t, Foldable t1) =>
t (RTVar tv (RTypeBV b v c tv (NoReftB b)), r)
-> t1 (PVarBV b v (RTypeBV b v c tv (NoReftB b)))
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
mkUnivs t (RTVar tv (RTypeBV b v c tv (NoReftB b)), r)
αs t1 (PVarBV b v (RTypeBV b v c tv (NoReftB b)))
πs RTypeBV b v c tv r
rt = ((RTVar tv (RTypeBV b v c tv (NoReftB b)), r)
 -> RTypeBV b v c tv r -> RTypeBV b v c tv r)
-> RTypeBV b v c tv r
-> t (RTVar tv (RTypeBV b v c tv (NoReftB b)), r)
-> RTypeBV b v c tv r
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(RTVar tv (RTypeBV b v c tv (NoReftB b))
a,r
r) RTypeBV b v c tv r
t -> RTVar tv (RTypeBV b v c tv (NoReftB b))
-> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
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 tv (RTypeBV b v c tv (NoReftB b))
a RTypeBV b v c tv r
t r
r) ((PVarBV b v (RTypeBV b v c tv (NoReftB b))
 -> RTypeBV b v c tv r -> RTypeBV b v c tv r)
-> RTypeBV b v c tv r
-> t1 (PVarBV b v (RTypeBV b v c tv (NoReftB b)))
-> RTypeBV b v c tv r
forall a b. (a -> b -> b) -> b -> t1 a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr PVarBV b v (RTypeBV b v c tv (NoReftB b))
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP RTypeBV b v c tv r
rt t1 (PVarBV b v (RTypeBV b v c tv (NoReftB b)))
πs) t (RTVar tv (RTypeBV b v c tv (NoReftB b)), r)
αs

bkUnivClass :: SpecType -> ([(SpecRTVar, RReft)],[PVar RSort], [(RTyCon, [SpecType])], SpecType )
bkUnivClass :: SpecType
-> ([(SpecRTVar, RReft)], [PVar RSort], [(RTyCon, [SpecType])],
    SpecType)
bkUnivClass SpecType
t        = ([(SpecRTVar, RReft)]
as, [PVar RSort]
ps, [(RTyCon, [SpecType])]
cs, SpecType
t2)
  where
    ([(SpecRTVar, RReft)]
as, [PVar RSort]
ps, SpecType
t1) = SpecType -> ([(SpecRTVar, RReft)], [PVar RSort], SpecType)
forall b v tv c r.
RTypeBV b v tv c r
-> ([(RTVar c (RTypeBV b v tv c (NoReftB b)), r)],
    [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r)
bkUniv  SpecType
t
    ([(RTyCon, [SpecType])]
cs, SpecType
t2)     = SpecType -> ([(RTyCon, [SpecType])], SpecType)
forall c b v tv r.
(PPrint c, TyConable c) =>
RTypeBV b v c tv r
-> ([(c, [RTypeBV b v c tv r])], RTypeBV b v c tv r)
bkClass SpecType
t1


bkUniv :: RTypeBV b v tv c r -> ([(RTVar c (RTypeBV b v tv c (NoReftB b)), r)], [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r)
bkUniv :: forall b v tv c r.
RTypeBV b v tv c r
-> ([(RTVar c (RTypeBV b v tv c (NoReftB b)), r)],
    [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r)
bkUniv (RAllT RTVUBV b v tv c
α RTypeBV b v tv c r
t r
r) = let ([(RTVUBV b v tv c, r)]
αs, [PVarBV b v (RTypeBV b v tv c (NoReftB b))]
πs, RTypeBV b v tv c r
t') = RTypeBV b v tv c r
-> ([(RTVUBV b v tv c, r)],
    [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r)
forall b v tv c r.
RTypeBV b v tv c r
-> ([(RTVar c (RTypeBV b v tv c (NoReftB b)), r)],
    [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r)
bkUniv RTypeBV b v tv c r
t in ((RTVUBV b v tv c
α, r
r)(RTVUBV b v tv c, r)
-> [(RTVUBV b v tv c, r)] -> [(RTVUBV b v tv c, r)]
forall a. a -> [a] -> [a]
:[(RTVUBV b v tv c, r)]
αs, [PVarBV b v (RTypeBV b v tv c (NoReftB b))]
πs, RTypeBV b v tv c r
t')
bkUniv (RAllP PVarBV b v (RTypeBV b v tv c (NoReftB b))
π RTypeBV b v tv c r
t)   = let ([(RTVUBV b v tv c, r)]
αs, [PVarBV b v (RTypeBV b v tv c (NoReftB b))]
πs, RTypeBV b v tv c r
t') = RTypeBV b v tv c r
-> ([(RTVUBV b v tv c, r)],
    [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r)
forall b v tv c r.
RTypeBV b v tv c r
-> ([(RTVar c (RTypeBV b v tv c (NoReftB b)), r)],
    [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r)
bkUniv RTypeBV b v tv c r
t in ([(RTVUBV b v tv c, r)]
αs, PVarBV b v (RTypeBV b v tv c (NoReftB b))
πPVarBV b v (RTypeBV b v tv c (NoReftB b))
-> [PVarBV b v (RTypeBV b v tv c (NoReftB b))]
-> [PVarBV b v (RTypeBV b v tv c (NoReftB b))]
forall a. a -> [a] -> [a]
:[PVarBV b v (RTypeBV b v tv c (NoReftB b))]
πs, RTypeBV b v tv c r
t')
bkUniv RTypeBV b v tv c r
t             = ([], [], RTypeBV b v tv c r
t)


-- bkFun :: RType t t1 a -> ([Symbol], [RType t t1 a], [a], RType t t1 a)
-- bkFun (RFun x t t' r) = let (xs, ts, rs, t'') = bkFun t'  in (x:xs, t:ts, r:rs, t'')
-- bkFun t               = ([], [], [], t)

bkUnivClass' :: SpecType ->
  ([(SpecRTVar, RReft)], [PVar RSort], [(Symbol, SpecType, RReft)], SpecType)
bkUnivClass' :: SpecType
-> ([(SpecRTVar, RReft)], [PVar RSort],
    [(Symbol, SpecType, RReft)], SpecType)
bkUnivClass' SpecType
t = ([(SpecRTVar, RReft)]
as, [PVar RSort]
ps, [Symbol] -> [SpecType] -> [RReft] -> [(Symbol, SpecType, RReft)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Symbol]
bs [SpecType]
ts [RReft]
rs, SpecType
t2)
  where
    ([(SpecRTVar, RReft)]
as, [PVar RSort]
ps, SpecType
t1) = SpecType -> ([(SpecRTVar, RReft)], [PVar RSort], SpecType)
forall b v tv c r.
RTypeBV b v tv c r
-> ([(RTVar c (RTypeBV b v tv c (NoReftB b)), r)],
    [PVarBV b v (RTypeBV b v tv c (NoReftB b))], RTypeBV b v tv c r)
bkUniv  SpecType
t
    ([Symbol]
bs, [SpecType]
ts, [RReft]
rs, SpecType
t2)     = SpecType -> ([Symbol], [SpecType], [RReft], SpecType)
forall t t1 a.
TyConable t =>
RType t t1 a -> ([Symbol], [RType t t1 a], [a], RType t t1 a)
bkClass' SpecType
t1

bkClass' :: TyConable t => RType t t1 a -> ([Symbol], [RType t t1 a], [a], RType t t1 a)
bkClass' :: forall t t1 a.
TyConable t =>
RType t t1 a -> ([Symbol], [RType t t1 a], [a], RType t t1 a)
bkClass' (RFun Symbol
x RFInfo
_ t :: RTypeBV Symbol Symbol t t1 a
t@(RApp t
c [RTypeBV Symbol Symbol t t1 a]
_ [RTPropBV Symbol Symbol t t1 a]
_ a
_) RTypeBV Symbol Symbol t t1 a
t' a
r)
  | t -> Bool
forall c. TyConable c => c -> Bool
isClass t
c
  = let ([Symbol]
xs, [RTypeBV Symbol Symbol t t1 a]
ts, [a]
rs, RTypeBV Symbol Symbol t t1 a
t'') = RTypeBV Symbol Symbol t t1 a
-> ([Symbol], [RTypeBV Symbol Symbol t t1 a], [a],
    RTypeBV Symbol Symbol t t1 a)
forall t t1 a.
TyConable t =>
RType t t1 a -> ([Symbol], [RType t t1 a], [a], RType t t1 a)
bkClass' RTypeBV Symbol Symbol t t1 a
t' in (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
xs, RTypeBV Symbol Symbol t t1 a
tRTypeBV Symbol Symbol t t1 a
-> [RTypeBV Symbol Symbol t t1 a] -> [RTypeBV Symbol Symbol t t1 a]
forall a. a -> [a] -> [a]
:[RTypeBV Symbol Symbol t t1 a]
ts, a
ra -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
rs, RTypeBV Symbol Symbol t t1 a
t'')
bkClass' (RRTy [(Symbol, RTypeBV Symbol Symbol t t1 a)]
e a
r Oblig
o RTypeBV Symbol Symbol t t1 a
t)
  = let ([Symbol]
xs, [RTypeBV Symbol Symbol t t1 a]
ts, [a]
rs, RTypeBV Symbol Symbol t t1 a
t'') = RTypeBV Symbol Symbol t t1 a
-> ([Symbol], [RTypeBV Symbol Symbol t t1 a], [a],
    RTypeBV Symbol Symbol t t1 a)
forall t t1 a.
TyConable t =>
RType t t1 a -> ([Symbol], [RType t t1 a], [a], RType t t1 a)
bkClass' RTypeBV Symbol Symbol t t1 a
t in ([Symbol]
xs, [RTypeBV Symbol Symbol t t1 a]
ts, [a]
rs, [(Symbol, RTypeBV Symbol Symbol t t1 a)]
-> a
-> Oblig
-> RTypeBV Symbol Symbol t t1 a
-> RTypeBV Symbol Symbol t t1 a
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 t t1 a)]
e a
r Oblig
o RTypeBV Symbol Symbol t t1 a
t'')
bkClass' RTypeBV Symbol Symbol t t1 a
t
  = ([], [],[],RTypeBV Symbol Symbol t t1 a
t)

bkClass :: (F.PPrint c, TyConable c) => RTypeBV b v c tv r -> ([(c, [RTypeBV b v c tv r])], RTypeBV b v c tv r)
bkClass :: forall c b v tv r.
(PPrint c, TyConable c) =>
RTypeBV b v c tv r
-> ([(c, [RTypeBV b v c tv r])], RTypeBV b v c tv r)
bkClass (RFun b
_ RFInfo
_ (RApp c
c [RTypeBV b v c tv r]
t [RTPropBV b v c tv r]
_ r
_) RTypeBV b v c tv r
t' r
_)
  | [Char] -> Bool -> Bool
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"IS-CLASS: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ c -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp c
c) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ c -> Bool
forall c. TyConable c => c -> Bool
isClass c
c
  = let ([(c, [RTypeBV b v c tv r])]
cs, RTypeBV b v c tv r
t'') = RTypeBV b v c tv r
-> ([(c, [RTypeBV b v c tv r])], RTypeBV b v c tv r)
forall c b v tv r.
(PPrint c, TyConable c) =>
RTypeBV b v c tv r
-> ([(c, [RTypeBV b v c tv r])], RTypeBV b v c tv r)
bkClass RTypeBV b v c tv r
t' in ((c
c, [RTypeBV b v c tv r]
t)(c, [RTypeBV b v c tv r])
-> [(c, [RTypeBV b v c tv r])] -> [(c, [RTypeBV b v c tv r])]
forall a. a -> [a] -> [a]
:[(c, [RTypeBV b v c tv r])]
cs, RTypeBV b v c tv r
t'')
bkClass (RRTy [(b, RTypeBV b v c tv r)]
e r
r Oblig
o RTypeBV b v c tv r
t)
  = let ([(c, [RTypeBV b v c tv r])]
cs, RTypeBV b v c tv r
t') = RTypeBV b v c tv r
-> ([(c, [RTypeBV b v c tv r])], RTypeBV b v c tv r)
forall c b v tv r.
(PPrint c, TyConable c) =>
RTypeBV b v c tv r
-> ([(c, [RTypeBV b v c tv r])], RTypeBV b v c tv r)
bkClass RTypeBV b v c tv r
t in ([(c, [RTypeBV b v c tv r])]
cs, [(b, RTypeBV b v c tv r)]
-> r -> Oblig -> RTypeBV b v c tv r -> RTypeBV b v c tv r
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 [(b, RTypeBV b v c tv r)]
e r
r Oblig
o RTypeBV b v c tv r
t')
bkClass RTypeBV b v c tv r
t
  = ([], RTypeBV b v c tv r
t)

rFun :: IsReft r => b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
rFun :: forall r b v c tv.
IsReft r =>
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
rFun b
b RTypeBV b v c tv r
t RTypeBV b v c tv r
t' = b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
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 b
b RFInfo
defRFInfo RTypeBV b v c tv r
t RTypeBV b v c tv r
t' r
forall r. IsReft r => r
trueReft

rFun' :: IsReft r => RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun' :: forall r c tv.
IsReft r =>
RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun' RFInfo
i Symbol
b RType c tv r
t RType c tv r
t' = Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
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 RType c tv r
t RType c tv r
t' r
forall r. IsReft r => r
trueReft

rFunDebug :: IsReft r => Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFunDebug :: forall r c tv.
IsReft r =>
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFunDebug Symbol
b RType c tv r
t RType c tv r
t' = Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
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 (Bool -> RFInfo
classRFInfo Bool
True) RType c tv r
t RType c tv r
t' r
forall r. IsReft r => r
trueReft

rCls :: IsReft r => Ghc.TyCon -> [RType RTyCon tv r] -> RType RTyCon tv r
rCls :: forall r tv.
IsReft r =>
TyCon -> [RType RTyCon tv r] -> RType RTyCon tv r
rCls TyCon
c [RType RTyCon tv r]
ts   = RTyCon
-> [RType RTyCon tv r]
-> [RTPropBV Symbol Symbol RTyCon tv r]
-> r
-> RType RTyCon tv r
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 (TyCon -> [PVar RSort] -> TyConInfo -> RTyCon
RTyCon TyCon
c [] TyConInfo
defaultTyConInfo) [RType RTyCon tv r]
ts [] r
forall r. IsReft r => r
trueReft

rRCls :: IsReft r => c -> [RType c tv r] -> RType c tv r
rRCls :: forall r c tv. IsReft r => c -> [RType c tv r] -> RType c tv r
rRCls c
rc [RType c tv r]
ts = c
-> [RType c tv r]
-> [RTPropBV Symbol Symbol c tv r]
-> r
-> RType c tv r
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 c
rc [RType c tv r]
ts [] r
forall r. IsReft r => r
trueReft

addInvCond :: SpecType -> RReft -> SpecType
addInvCond :: SpecType -> RReft -> SpecType
addInvCond SpecType
t RReft
r'
  | ReftBV Symbol Symbol -> Bool
forall r. ToReft r => r -> Bool
isTauto (ReftBV Symbol Symbol -> Bool) -> ReftBV Symbol Symbol -> Bool
forall a b. (a -> b) -> a -> b
$ RReft -> ReftBV Symbol Symbol
forall b v r. UReftBV b v r -> r
ur_reft RReft
r' -- null rv
  = SpecType
t
  | Bool
otherwise
  = RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> SpecType
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
fromRTypeRep (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> SpecType)
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep {ty_res = RRTy [(x', tbd)] r OInv tbd}
  where
    trep :: RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep = SpecType -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep SpecType
t
    tbd :: SpecType
tbd  = RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> SpecType
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
ty_res RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep
    r :: RReft
r    = RReft
r' {ur_reft = F.Reft (v, rx)}
    su :: (Symbol, ExprBV Symbol Symbol)
su   = (Symbol
v, Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
F.EVar Symbol
x')
    x' :: Symbol
x'   = Symbol
"xInv"
    rx :: ExprBV Symbol Symbol
rx   = 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
v) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol)
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall a b. (a -> b) -> a -> b
$ ExprBV Symbol Symbol
-> (Variable (ExprBV Symbol Symbol),
    ExprBV
      (Variable (ExprBV Symbol Symbol))
      (Variable (ExprBV Symbol Symbol)))
-> ExprBV Symbol Symbol
forall a.
Subable a =>
a -> (Variable a, ExprBV (Variable a) (Variable a)) -> a
F.subst1 ExprBV Symbol Symbol
rv (Symbol, ExprBV Symbol Symbol)
(Variable (ExprBV Symbol Symbol),
 ExprBV
   (Variable (ExprBV Symbol Symbol))
   (Variable (ExprBV Symbol Symbol)))
su
    F.Reft(Symbol
v, ExprBV Symbol Symbol
rv) = RReft -> ReftBV Symbol Symbol
forall b v r. UReftBV b v r -> r
ur_reft RReft
r'


instance (IsReft r, F.Subable r, TyConable c, F.Binder v, F.Variable r ~ v, ReftBind r ~ v) => F.Subable (RTPropBV v v c tv r) where
  type Variable (RTPropBV v v c tv r) = v
  syms :: RTPropBV v v c tv r -> [Variable (RTPropBV v v c tv r)]
syms (RProp  [(v, RTypeBV v v c tv (NoReftB v))]
ss RTypeBV v v c tv r
r)     = ((v, RTypeBV v v c tv (NoReftB v)) -> v
forall a b. (a, b) -> a
fst ((v, RTypeBV v v c tv (NoReftB v)) -> v)
-> [(v, RTypeBV v v c tv (NoReftB v))] -> [v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(v, RTypeBV v v c tv (NoReftB v))]
ss) [v] -> [v] -> [v]
forall a. [a] -> [a] -> [a]
++ RTypeBV v v c tv r -> [Variable (RTypeBV v v c tv r)]
forall a. Subable a => a -> [Variable a]
F.syms RTypeBV v v c tv r
r

  subst :: HasCallStack =>
SubstV (Variable (RTPropBV v v c tv r))
-> RTPropBV v v c tv r -> RTPropBV v v c tv r
subst SubstV (Variable (RTPropBV v v c tv r))
su (RProp [(v, RTypeBV v v c tv (NoReftB v))]
ss (RHole r
r)) = [(v, RTypeBV v v c tv (NoReftB v))]
-> RTypeBV v v c tv r -> RTPropBV v v c tv r
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(v, RTypeBV v v c tv (NoReftB v))]
ss (r -> RTypeBV v v c tv r
forall b v c tv r. r -> RTypeBV b v c tv r
RHole (SubstV (Variable r) -> r -> r
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst SubstV (Variable r)
SubstV (Variable (RTPropBV v v c tv r))
su r
r))
  subst SubstV (Variable (RTPropBV v v c tv r))
su (RProp  [(v, RTypeBV v v c tv (NoReftB v))]
ss RTypeBV v v c tv r
t) = [(v, RTypeBV v v c tv (NoReftB v))]
-> RTypeBV v v c tv r -> RTPropBV v v c tv r
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(v, RTypeBV v v c tv (NoReftB v))]
ss (SubstV (Variable r) -> r -> r
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst SubstV (Variable r)
SubstV (Variable (RTPropBV v v c tv r))
su (r -> r) -> RTypeBV v v c tv r -> RTypeBV v v c tv r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTypeBV v v c tv r
t)

  substf :: (Variable (RTPropBV v v c tv r)
 -> ExprBV
      (Variable (RTPropBV v v c tv r)) (Variable (RTPropBV v v c tv r)))
-> RTPropBV v v c tv r -> RTPropBV v v c tv r
substf Variable (RTPropBV v v c tv r)
-> ExprBV
     (Variable (RTPropBV v v c tv r)) (Variable (RTPropBV v v c tv r))
f (RProp [(v, RTypeBV v v c tv (NoReftB v))]
ss (RHole r
r)) = [(v, RTypeBV v v c tv (NoReftB v))]
-> RTypeBV v v c tv r -> RTPropBV v v c tv r
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(v, RTypeBV v v c tv (NoReftB v))]
ss (r -> RTypeBV v v c tv r
forall b v c tv r. r -> RTypeBV b v c tv r
RHole ((Variable r -> ExprBV (Variable r) (Variable r)) -> r -> r
forall a.
Subable a =>
(Variable a -> ExprBV (Variable a) (Variable a)) -> a -> a
F.substf Variable r -> ExprBV (Variable r) (Variable r)
Variable (RTPropBV v v c tv r)
-> ExprBV
     (Variable (RTPropBV v v c tv r)) (Variable (RTPropBV v v c tv r))
f r
r))
  substf Variable (RTPropBV v v c tv r)
-> ExprBV
     (Variable (RTPropBV v v c tv r)) (Variable (RTPropBV v v c tv r))
f (RProp  [(v, RTypeBV v v c tv (NoReftB v))]
ss RTypeBV v v c tv r
t) = [(v, RTypeBV v v c tv (NoReftB v))]
-> RTypeBV v v c tv r -> RTPropBV v v c tv r
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(v, RTypeBV v v c tv (NoReftB v))]
ss ((Variable r -> ExprBV (Variable r) (Variable r)) -> r -> r
forall a.
Subable a =>
(Variable a -> ExprBV (Variable a) (Variable a)) -> a -> a
F.substf Variable r -> ExprBV (Variable r) (Variable r)
Variable (RTPropBV v v c tv r)
-> ExprBV
     (Variable (RTPropBV v v c tv r)) (Variable (RTPropBV v v c tv r))
f (r -> r) -> RTypeBV v v c tv r -> RTypeBV v v c tv r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTypeBV v v c tv r
t)

  substa :: (Variable (RTPropBV v v c tv r) -> Variable (RTPropBV v v c tv r))
-> RTPropBV v v c tv r -> RTPropBV v v c tv r
substa Variable (RTPropBV v v c tv r) -> Variable (RTPropBV v v c tv r)
f (RProp [(v, RTypeBV v v c tv (NoReftB v))]
ss (RHole r
r)) = [(v, RTypeBV v v c tv (NoReftB v))]
-> RTypeBV v v c tv r -> RTPropBV v v c tv r
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(v, RTypeBV v v c tv (NoReftB v))]
ss (r -> RTypeBV v v c tv r
forall b v c tv r. r -> RTypeBV b v c tv r
RHole ((Variable r -> Variable r) -> r -> r
forall a. Subable a => (Variable a -> Variable a) -> a -> a
F.substa Variable r -> Variable r
Variable (RTPropBV v v c tv r) -> Variable (RTPropBV v v c tv r)
f r
r))
  substa Variable (RTPropBV v v c tv r) -> Variable (RTPropBV v v c tv r)
f (RProp  [(v, RTypeBV v v c tv (NoReftB v))]
ss RTypeBV v v c tv r
t) = [(v, RTypeBV v v c tv (NoReftB v))]
-> RTypeBV v v c tv r -> RTPropBV v v c tv r
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(v, RTypeBV v v c tv (NoReftB v))]
ss ((Variable r -> Variable r) -> r -> r
forall a. Subable a => (Variable a -> Variable a) -> a -> a
F.substa Variable r -> Variable r
Variable (RTPropBV v v c tv r) -> Variable (RTPropBV v v c tv r)
f (r -> r) -> RTypeBV v v c tv r -> RTypeBV v v c tv r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTypeBV v v c tv r
t)


instance (F.Subable r, IsReft r, TyConable c, F.Binder v, F.Variable r ~ v, ReftBind r ~ v) => F.Subable (RTypeBV v v c tv r) where
  type Variable (RTypeBV v v c tv r) = v
  syms :: RTypeBV v v c tv r -> [Variable (RTypeBV v v c tv r)]
syms        = Bool
-> (SEnvB v (RTypeBV v v c tv r) -> r -> [v] -> [v])
-> [v]
-> RTypeBV v v c tv r
-> [v]
forall r c b v tv z.
(IsReft r, TyConable c, Binder b, ReftBind r ~ b) =>
Bool
-> (SEnvB b (RTypeBV b v c tv r) -> r -> z -> z)
-> z
-> RTypeBV b v c tv r
-> z
foldReft Bool
False (\SEnvB v (RTypeBV v v c tv r)
_ r
r [v]
acc -> r -> [Variable r]
forall a. Subable a => a -> [Variable a]
F.syms r
r [v] -> [v] -> [v]
forall a. [a] -> [a] -> [a]
++ [v]
acc) []
  -- 'substa' will substitute bound vars
  substa :: (Variable (RTypeBV v v c tv r) -> Variable (RTypeBV v v c tv r))
-> RTypeBV v v c tv r -> RTypeBV v v c tv r
substa Variable (RTypeBV v v c tv r) -> Variable (RTypeBV v v c tv r)
f    = ([v] -> ExprBV v v -> ExprBV v v)
-> [v] -> RTypeBV v v c tv r -> RTypeBV v v c tv r
forall b v c tv r.
([b] -> ExprBV b v -> ExprBV b v)
-> [b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
emapExprArg (\[v]
_ -> (Variable (ExprBV v v) -> Variable (ExprBV v v))
-> ExprBV v v -> ExprBV v v
forall a. Subable a => (Variable a -> Variable a) -> a -> a
F.substa Variable (ExprBV v v) -> Variable (ExprBV v v)
Variable (RTypeBV v v c tv r) -> Variable (RTypeBV v v c tv r)
f) []      (RTypeBV v v c tv r -> RTypeBV v v c tv r)
-> (RTypeBV v v c tv r -> RTypeBV v v c tv r)
-> RTypeBV v v c tv r
-> RTypeBV v v c tv r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (r -> r) -> RTypeBV v v c tv r -> RTypeBV v v c tv r
forall r1 r2 b v c tv.
(r1 -> r2) -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
mapReft  ((Variable r -> Variable r) -> r -> r
forall a. Subable a => (Variable a -> Variable a) -> a -> a
F.substa Variable r -> Variable r
Variable (RTypeBV v v c tv r) -> Variable (RTypeBV v v c tv r)
f)
  -- 'substf' will NOT substitute bound vars
  substf :: (Variable (RTypeBV v v c tv r)
 -> ExprBV
      (Variable (RTypeBV v v c tv r)) (Variable (RTypeBV v v c tv r)))
-> RTypeBV v v c tv r -> RTypeBV v v c tv r
substf Variable (RTypeBV v v c tv r)
-> ExprBV
     (Variable (RTypeBV v v c tv r)) (Variable (RTypeBV v v c tv r))
f    = ([v] -> ExprBV v v -> ExprBV v v)
-> [v] -> RTypeBV v v c tv r -> RTypeBV v v c tv r
forall b v c tv r.
([b] -> ExprBV b v -> ExprBV b v)
-> [b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
emapExprArg (\[v]
_ -> (Variable (ExprBV v v)
 -> ExprBV (Variable (ExprBV v v)) (Variable (ExprBV v v)))
-> ExprBV v v -> ExprBV v v
forall a.
Subable a =>
(Variable a -> ExprBV (Variable a) (Variable a)) -> a -> a
F.substf Variable (ExprBV v v)
-> ExprBV (Variable (ExprBV v v)) (Variable (ExprBV v v))
Variable (RTypeBV v v c tv r)
-> ExprBV
     (Variable (RTypeBV v v c tv r)) (Variable (RTypeBV v v c tv r))
f) []      (RTypeBV v v c tv r -> RTypeBV v v c tv r)
-> (RTypeBV v v c tv r -> RTypeBV v v c tv r)
-> RTypeBV v v c tv r
-> RTypeBV v v c tv r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([v] -> r -> r) -> [v] -> RTypeBV v v c tv r -> RTypeBV v v c tv r
forall b r1 r2 v c tv.
([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft ((v -> ExprBV v v) -> r -> r
(Variable r -> ExprBV (Variable r) (Variable r)) -> r -> r
forall a.
Subable a =>
(Variable a -> ExprBV (Variable a) (Variable a)) -> a -> a
F.substf ((v -> ExprBV v v) -> r -> r)
-> ([v] -> v -> ExprBV v v) -> [v] -> r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (v -> ExprBV v v) -> [v] -> v -> ExprBV v v
forall v b. Eq v => (v -> ExprBV b v) -> [v] -> v -> ExprBV b v
F.substfExcept v -> ExprBV v v
Variable (RTypeBV v v c tv r)
-> ExprBV
     (Variable (RTypeBV v v c tv r)) (Variable (RTypeBV v v c tv r))
f) []
  subst :: HasCallStack =>
SubstV (Variable (RTypeBV v v c tv r))
-> RTypeBV v v c tv r -> RTypeBV v v c tv r
subst SubstV (Variable (RTypeBV v v c tv r))
su    = ([v] -> ExprBV v v -> ExprBV v v)
-> [v] -> RTypeBV v v c tv r -> RTypeBV v v c tv r
forall b v c tv r.
([b] -> ExprBV b v -> ExprBV b v)
-> [b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
emapExprArg (\[v]
_ -> SubstV (Variable (ExprBV v v)) -> ExprBV v v -> ExprBV v v
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst SubstV (Variable (ExprBV v v))
SubstV (Variable (RTypeBV v v c tv r))
su) []      (RTypeBV v v c tv r -> RTypeBV v v c tv r)
-> (RTypeBV v v c tv r -> RTypeBV v v c tv r)
-> RTypeBV v v c tv r
-> RTypeBV v v c tv r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([v] -> r -> r) -> [v] -> RTypeBV v v c tv r -> RTypeBV v v c tv r
forall b r1 r2 v c tv.
([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft (SubstV v -> r -> r
SubstV (Variable r) -> r -> r
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst  (SubstV v -> r -> r) -> ([v] -> SubstV v) -> [v] -> r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubstV v -> [v] -> SubstV v
forall v. Eq v => SubstV v -> [v] -> SubstV v
F.substExcept SubstV v
SubstV (Variable (RTypeBV v v c tv r))
su) []
  subst1 :: RTypeBV v v c tv r
-> (Variable (RTypeBV v v c tv r),
    ExprBV
      (Variable (RTypeBV v v c tv r)) (Variable (RTypeBV v v c tv r)))
-> RTypeBV v v c tv r
subst1 RTypeBV v v c tv r
t (Variable (RTypeBV v v c tv r),
 ExprBV
   (Variable (RTypeBV v v c tv r)) (Variable (RTypeBV v v c tv r)))
su = ([v] -> ExprBV v v -> ExprBV v v)
-> [v] -> RTypeBV v v c tv r -> RTypeBV v v c tv r
forall b v c tv r.
([b] -> ExprBV b v -> ExprBV b v)
-> [b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
emapExprArg (\[v]
_ ExprBV v v
e -> ExprBV v v
-> (Variable (ExprBV v v),
    ExprBV (Variable (ExprBV v v)) (Variable (ExprBV v v)))
-> ExprBV v v
forall a.
Subable a =>
a -> (Variable a, ExprBV (Variable a) (Variable a)) -> a
F.subst1 ExprBV v v
e (Variable (ExprBV v v),
 ExprBV (Variable (ExprBV v v)) (Variable (ExprBV v v)))
(Variable (RTypeBV v v c tv r),
 ExprBV
   (Variable (RTypeBV v v c tv r)) (Variable (RTypeBV v v c tv r)))
su) [] (RTypeBV v v c tv r -> RTypeBV v v c tv r)
-> RTypeBV v v c tv r -> RTypeBV v v c tv r
forall a b. (a -> b) -> a -> b
$ ([v] -> r -> r) -> [v] -> RTypeBV v v c tv r -> RTypeBV v v c tv r
forall b r1 r2 v c tv.
([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft (\[v]
xs r
r -> [Variable r]
-> r -> (Variable r, ExprBV (Variable r) (Variable r)) -> r
forall a.
Subable a =>
[Variable a]
-> a -> (Variable a, ExprBV (Variable a) (Variable a)) -> a
F.subst1Except [v]
[Variable r]
xs r
r (Variable r, ExprBV (Variable r) (Variable r))
(Variable (RTypeBV v v c tv r),
 ExprBV
   (Variable (RTypeBV v v c tv r)) (Variable (RTypeBV v v c tv r)))
su) [] RTypeBV v v c tv r
t


--------------------------------------------------------------------------------
-- | Visitors ------------------------------------------------------------------
--------------------------------------------------------------------------------
mapExprReft :: (b -> ExprBV b v -> ExprBV b v) -> RTypeBV b v c tv (RReftBV b v) -> RTypeBV b v c tv (RReftBV b v)
mapExprReft :: forall b v c tv.
(b -> ExprBV b v -> ExprBV b v)
-> RTypeBV b v c tv (RReftBV b v) -> RTypeBV b v c tv (RReftBV b v)
mapExprReft b -> ExprBV b v -> ExprBV b v
f = (RReftBV b v -> RReftBV b v)
-> RTypeBV b v c tv (RReftBV b v) -> RTypeBV b v c tv (RReftBV b v)
forall r1 r2 b v c tv.
(r1 -> r2) -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
mapReft RReftBV b v -> RReftBV b v
g
  where
    g :: RReftBV b v -> RReftBV b v
g (MkUReft (F.Reft (b
x, ExprBV b v
e)) PredicateBV b v
p) = ReftBV b v -> PredicateBV b v -> RReftBV b v
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft ((b, ExprBV b v) -> ReftBV b v
forall b v. (b, ExprBV b v) -> ReftBV b v
F.Reft (b
x, b -> ExprBV b v -> ExprBV b v
f b
x ExprBV b v
e)) PredicateBV b v
p

data OrReftBV r = LeftReftBV (F.ReftBV (ReftBind r) (ReftVar r)) | RightR r

instance ToReft r => ToReft (OrReftBV r) where
  type ReftBind (OrReftBV r) = ReftBind r
  type ReftVar (OrReftBV r) = ReftVar r
  toReft :: OrReftBV r -> ReftBV (ReftBind (OrReftBV r)) (ReftVar (OrReftBV r))
toReft (LeftReftBV ReftBV (ReftBind r) (ReftVar r)
r) = ReftBV (ReftBind r) (ReftVar r)
ReftBV (ReftBind (OrReftBV r)) (ReftVar (OrReftBV r))
r
  toReft (RightR r
r) = r -> ReftBV (ReftBind r) (ReftVar r)
forall r. ToReft r => r -> ReftBV (ReftBind r) (ReftVar r)
toReft r
r
  toUReft :: OrReftBV r
-> UReftBV
     (ReftBind (OrReftBV r))
     (ReftVar (OrReftBV r))
     (ReftBV (ReftBind (OrReftBV r)) (ReftVar (OrReftBV r)))
toUReft (LeftReftBV ReftBV (ReftBind r) (ReftVar r)
r) = ReftBV (ReftBind r) (ReftVar r)
-> PredicateBV (ReftBind r) (ReftVar r)
-> UReftBV
     (ReftBind r) (ReftVar r) (ReftBV (ReftBind r) (ReftVar r))
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft ReftBV (ReftBind r) (ReftVar r)
r ([UsedPVarBV (ReftBind r) (ReftVar r)]
-> PredicateBV (ReftBind r) (ReftVar r)
forall b v. [UsedPVarBV b v] -> PredicateBV b v
Pr [])
  toUReft (RightR r
r) = r
-> UReftBV
     (ReftBind r) (ReftVar r) (ReftBV (ReftBind r) (ReftVar r))
forall r.
ToReft r =>
r
-> UReftBV
     (ReftBind r) (ReftVar r) (ReftBV (ReftBind r) (ReftVar r))
toUReft r
r

instance ToReft r => Semigroup (OrReftBV r) where
  OrReftBV r
_ <> :: OrReftBV r -> OrReftBV r -> OrReftBV r
<> OrReftBV r
_ = [Char] -> OrReftBV r
forall a. HasCallStack => [Char] -> a
Prelude.error [Char]
"Meet OrReftBV"

instance ToReft r => Meet (OrReftBV r) where

instance F.Binder (ReftBind r) => Top (OrReftBV r) where
  top :: OrReftBV r -> OrReftBV r
top OrReftBV r
_ = ReftBV (ReftBind r) (ReftVar r) -> OrReftBV r
forall r. ReftBV (ReftBind r) (ReftVar r) -> OrReftBV r
LeftReftBV ReftBV (ReftBind r) (ReftVar r)
forall b v. Binder b => ReftBV b v
F.trueReft

instance ToReft r => IsReft (OrReftBV r) where
  ofReft :: ReftBV (ReftBind (OrReftBV r)) (ReftVar (OrReftBV r)) -> OrReftBV r
ofReft ReftBV (ReftBind (OrReftBV r)) (ReftVar (OrReftBV r))
r = ReftBV (ReftBind r) (ReftVar r) -> OrReftBV r
forall r. ReftBV (ReftBind r) (ReftVar r) -> OrReftBV r
LeftReftBV ReftBV (ReftBind r) (ReftVar r)
ReftBV (ReftBind (OrReftBV r)) (ReftVar (OrReftBV r))
r

isTrivial :: (ToReft r, TyConable c, F.Binder b, ReftBind r ~ b) => RTypeBV b v c tv r -> Bool
isTrivial :: forall r c b v tv.
(ToReft r, TyConable c, Binder b, ReftBind r ~ b) =>
RTypeBV b v c tv r -> Bool
isTrivial = Bool
-> (SEnvB b (RTypeBV b v c tv (OrReftBV r))
    -> OrReftBV r -> Bool -> Bool)
-> Bool
-> RTypeBV b v c tv (OrReftBV r)
-> Bool
forall r c b v tv z.
(IsReft r, TyConable c, Binder b, ReftBind r ~ b) =>
Bool
-> (SEnvB b (RTypeBV b v c tv r) -> r -> z -> z)
-> z
-> RTypeBV b v c tv r
-> z
foldReft Bool
False (\SEnvB b (RTypeBV b v c tv (OrReftBV r))
_ OrReftBV r
r Bool
b -> OrReftBV r -> Bool
forall r. ToReft r => r -> Bool
isTauto OrReftBV r
r Bool -> Bool -> Bool
&& Bool
b) Bool
True (RTypeBV b v c tv (OrReftBV r) -> Bool)
-> (RTypeBV b v c tv r -> RTypeBV b v c tv (OrReftBV r))
-> RTypeBV b v c tv r
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (r -> OrReftBV r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv (OrReftBV r)
forall a b. (a -> b) -> RTypeBV b v c tv a -> RTypeBV b v c tv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap r -> OrReftBV r
forall r. r -> OrReftBV r
RightR

mapReft ::  (r1 -> r2) -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
mapReft :: forall r1 r2 b v c tv.
(r1 -> r2) -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
mapReft r1 -> r2
f = ([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
forall b r1 r2 v c tv.
([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft ((r1 -> r2) -> [b] -> r1 -> r2
forall a b. a -> b -> a
const r1 -> r2
f) []

instance Top r => Top (RTypeBV b v c tv r) where
  top :: RTypeBV b v c tv r -> RTypeBV b v c tv r
top (RHole r
_) = Maybe SrcSpan -> [Char] -> RTypeBV b v c tv r
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"top called on (RProp _ (RHole _))"
  top RTypeBV b v c tv r
t = (r -> r) -> RTypeBV b v c tv r -> RTypeBV b v c tv r
forall r1 r2 b v c tv.
(r1 -> r2) -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
mapReft r -> r
forall r. Top r => r -> r
top RTypeBV b v c tv r
t

emapReft ::  ([b] -> r1 -> r2) -> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft :: forall b r1 r2 v c tv.
([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft [b] -> r1 -> r2
f [b]
γ (RVar tv
α r1
r)        = tv -> r2 -> RTypeBV b v c tv r2
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar  tv
α ([b] -> r1 -> r2
f [b]
γ r1
r)
emapReft [b] -> r1 -> r2
f [b]
γ (RAllT RTVUBV b v c tv
α RTypeBV b v c tv r1
t r1
r)     = RTVUBV b v c tv -> RTypeBV b v c tv r2 -> r2 -> RTypeBV b v c tv r2
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 RTVUBV b v c tv
α (([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
forall b r1 r2 v c tv.
([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft [b] -> r1 -> r2
f [b]
γ RTypeBV b v c tv r1
t) ([b] -> r1 -> r2
f [b]
γ r1
r)
emapReft [b] -> r1 -> r2
f [b]
γ (RAllP PVUBV b v c tv
π RTypeBV b v c tv r1
t)       = PVUBV b v c tv -> RTypeBV b v c tv r2 -> RTypeBV b v c tv r2
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP PVUBV b v c tv
π (([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
forall b r1 r2 v c tv.
([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft [b] -> r1 -> r2
f [b]
γ RTypeBV b v c tv r1
t)
emapReft [b] -> r1 -> r2
f [b]
γ (RFun b
x RFInfo
i RTypeBV b v c tv r1
t RTypeBV b v c tv r1
t' r1
r) = b
-> RFInfo
-> RTypeBV b v c tv r2
-> RTypeBV b v c tv r2
-> r2
-> RTypeBV b v c tv r2
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  b
x RFInfo
i (([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
forall b r1 r2 v c tv.
([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft [b] -> r1 -> r2
f [b]
γ RTypeBV b v c tv r1
t) (([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
forall b r1 r2 v c tv.
([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft [b] -> r1 -> r2
f (b
xb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
γ) RTypeBV b v c tv r1
t') ([b] -> r1 -> r2
f (b
xb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
γ) r1
r)
emapReft [b] -> r1 -> r2
f [b]
γ (RApp c
c [RTypeBV b v c tv r1]
ts [RTPropBV b v c tv r1]
rs r1
r)  = c
-> [RTypeBV b v c tv r2]
-> [RTPropBV b v c tv r2]
-> r2
-> RTypeBV b v c tv r2
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  c
c (([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
forall b r1 r2 v c tv.
([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft [b] -> r1 -> r2
f [b]
γ (RTypeBV b v c tv r1 -> RTypeBV b v c tv r2)
-> [RTypeBV b v c tv r1] -> [RTypeBV b v c tv r2]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeBV b v c tv r1]
ts) (([b] -> r1 -> r2)
-> [b] -> RTPropBV b v c tv r1 -> RTPropBV b v c tv r2
forall b t s v c tv.
([b] -> t -> s)
-> [b] -> RTPropBV b v c tv t -> RTPropBV b v c tv s
emapRef [b] -> r1 -> r2
f [b]
γ (RTPropBV b v c tv r1 -> RTPropBV b v c tv r2)
-> [RTPropBV b v c tv r1] -> [RTPropBV b v c tv r2]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropBV b v c tv r1]
rs) ([b] -> r1 -> r2
f [b]
γ r1
r)
emapReft [b] -> r1 -> r2
f [b]
γ (RAllE b
z RTypeBV b v c tv r1
t RTypeBV b v c tv r1
t')    = b
-> RTypeBV b v c tv r2
-> RTypeBV b v c tv r2
-> RTypeBV b v c tv r2
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 b
z (([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
forall b r1 r2 v c tv.
([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft [b] -> r1 -> r2
f [b]
γ RTypeBV b v c tv r1
t) (([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
forall b r1 r2 v c tv.
([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft [b] -> r1 -> r2
f [b]
γ RTypeBV b v c tv r1
t')
emapReft [b] -> r1 -> r2
f [b]
γ (REx b
z RTypeBV b v c tv r1
t RTypeBV b v c tv r1
t')      = b
-> RTypeBV b v c tv r2
-> RTypeBV b v c tv r2
-> RTypeBV b v c tv r2
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   b
z (([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
forall b r1 r2 v c tv.
([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft [b] -> r1 -> r2
f [b]
γ RTypeBV b v c tv r1
t) (([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
forall b r1 r2 v c tv.
([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft [b] -> r1 -> r2
f [b]
γ RTypeBV b v c tv r1
t')
emapReft [b] -> r1 -> r2
_ [b]
_ (RExprArg Located (ExprBV b v)
e)      = Located (ExprBV b v) -> RTypeBV b v c tv r2
forall b v c tv r. Located (ExprBV b v) -> RTypeBV b v c tv r
RExprArg Located (ExprBV b v)
e
emapReft [b] -> r1 -> r2
f [b]
γ (RAppTy RTypeBV b v c tv r1
t RTypeBV b v c tv r1
t' r1
r)   = RTypeBV b v c tv r2
-> RTypeBV b v c tv r2 -> r2 -> RTypeBV b v c tv r2
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 (([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
forall b r1 r2 v c tv.
([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft [b] -> r1 -> r2
f [b]
γ RTypeBV b v c tv r1
t) (([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
forall b r1 r2 v c tv.
([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft [b] -> r1 -> r2
f [b]
γ RTypeBV b v c tv r1
t') ([b] -> r1 -> r2
f [b]
γ r1
r)
emapReft [b] -> r1 -> r2
f [b]
γ (RRTy [(b, RTypeBV b v c tv r1)]
e r1
r Oblig
o RTypeBV b v c tv r1
t)    = [(b, RTypeBV b v c tv r2)]
-> r2 -> Oblig -> RTypeBV b v c tv r2 -> RTypeBV b v c tv r2
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  ((RTypeBV b v c tv r1 -> RTypeBV b v c tv r2)
-> (b, RTypeBV b v c tv r1) -> (b, RTypeBV b v c tv r2)
forall a b. (a -> b) -> (b, a) -> (b, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
forall b r1 r2 v c tv.
([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft [b] -> r1 -> r2
f [b]
γ) ((b, RTypeBV b v c tv r1) -> (b, RTypeBV b v c tv r2))
-> [(b, RTypeBV b v c tv r1)] -> [(b, RTypeBV b v c tv r2)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(b, RTypeBV b v c tv r1)]
e) ([b] -> r1 -> r2
f [b]
γ r1
r) Oblig
o (([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
forall b r1 r2 v c tv.
([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft [b] -> r1 -> r2
f [b]
γ RTypeBV b v c tv r1
t)
emapReft [b] -> r1 -> r2
f [b]
γ (RHole r1
r)         = r2 -> RTypeBV b v c tv r2
forall b v c tv r. r -> RTypeBV b v c tv r
RHole ([b] -> r1 -> r2
f [b]
γ r1
r)

emapRef :: ([b] -> t -> s) ->  [b] -> RTPropBV b v c tv t -> RTPropBV b v c tv s
emapRef :: forall b t s v c tv.
([b] -> t -> s)
-> [b] -> RTPropBV b v c tv t -> RTPropBV b v c tv s
emapRef  [b] -> t -> s
f [b]
γ (RProp [(b, RTypeBV b v c tv (NoReftB b))]
s (RHole t
r))  = [(b, RTypeBV b v c tv (NoReftB b))]
-> RTypeBV b v c tv s
-> RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv s)
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(b, RTypeBV b v c tv (NoReftB b))]
s (RTypeBV b v c tv s
 -> RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv s))
-> RTypeBV b v c tv s
-> RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv s)
forall a b. (a -> b) -> a -> b
$ s -> RTypeBV b v c tv s
forall b v c tv r. r -> RTypeBV b v c tv r
RHole ([b] -> t -> s
f [b]
γ t
r)
emapRef  [b] -> t -> s
f [b]
γ (RProp [(b, RTypeBV b v c tv (NoReftB b))]
s RTypeBV b v c tv t
t)         = [(b, RTypeBV b v c tv (NoReftB b))]
-> RTypeBV b v c tv s
-> RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv s)
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(b, RTypeBV b v c tv (NoReftB b))]
s (RTypeBV b v c tv s
 -> RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv s))
-> RTypeBV b v c tv s
-> RefB b (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv s)
forall a b. (a -> b) -> a -> b
$ ([b] -> t -> s) -> [b] -> RTypeBV b v c tv t -> RTypeBV b v c tv s
forall b r1 r2 v c tv.
([b] -> r1 -> r2)
-> [b] -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
emapReft [b] -> t -> s
f [b]
γ RTypeBV b v c tv t
t

mapRTypeV ::  (v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV :: forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV v -> v'
_ (RVar tv
α r
r)        = tv -> r -> RTypeBV b v' c tv r
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar tv
α r
r
mapRTypeV v -> v'
f (RAllT RTVUBV b v c tv
α RTypeBV b v c tv r
t r
r)     = RTVUBV b v' c tv -> RTypeBV b v' c tv r -> r -> RTypeBV b v' c tv r
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 ((RTypeBV b v c tv (NoReftB b) -> RTypeBV b v' c tv (NoReftB b))
-> RTVUBV b v c tv -> RTVUBV b v' c tv
forall a b. (a -> b) -> RTVar tv a -> RTVar tv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((v -> v')
-> RTypeBV b v c tv (NoReftB b) -> RTypeBV b v' c tv (NoReftB b)
forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV v -> v'
f) RTVUBV b v c tv
α) ((v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV v -> v'
f RTypeBV b v c tv r
t) r
r
mapRTypeV v -> v'
f (RAllP PVUBV b v c tv
π RTypeBV b v c tv r
t)       = PVUBV b v' c tv -> RTypeBV b v' c tv r -> RTypeBV b v' c tv r
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP ((v -> v')
-> (RTypeBV b v c tv (NoReftB b) -> RTypeBV b v' c tv (NoReftB b))
-> PVUBV b v c tv
-> PVUBV b v' c tv
forall v v' t t' b.
(v -> v') -> (t -> t') -> PVarBV b v t -> PVarBV b v' t'
mapPVarV v -> v'
f ((v -> v')
-> RTypeBV b v c tv (NoReftB b) -> RTypeBV b v' c tv (NoReftB b)
forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV v -> v'
f) PVUBV b v c tv
π) ((v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV v -> v'
f RTypeBV b v c tv r
t)
mapRTypeV v -> v'
f (RFun b
x RFInfo
i RTypeBV b v c tv r
t RTypeBV b v c tv r
t' r
r) = b
-> RFInfo
-> RTypeBV b v' c tv r
-> RTypeBV b v' c tv r
-> r
-> RTypeBV b v' c tv r
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 b
x RFInfo
i ((v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV v -> v'
f RTypeBV b v c tv r
t) ((v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV v -> v'
f RTypeBV b v c tv r
t') r
r
mapRTypeV v -> v'
f (RApp c
c [RTypeBV b v c tv r]
ts [RTPropBV b v c tv r]
rs r
r)  = c
-> [RTypeBV b v' c tv r]
-> [RTPropBV b v' c tv r]
-> r
-> RTypeBV b v' c tv r
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 c
c ((v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV v -> v'
f (RTypeBV b v c tv r -> RTypeBV b v' c tv r)
-> [RTypeBV b v c tv r] -> [RTypeBV b v' c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeBV b v c tv r]
ts) (RTPropBV b v c tv r -> RTPropBV b v' c tv r
mapRefV (RTPropBV b v c tv r -> RTPropBV b v' c tv r)
-> [RTPropBV b v c tv r] -> [RTPropBV b v' c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropBV b v c tv r]
rs) r
r
  where
    mapRefV :: RTPropBV b v c tv r -> RTPropBV b v' c tv r
mapRefV (RProp [(b, RTypeBV b v c tv (NoReftB b))]
ss RTypeBV b v c tv r
t) = [(b, RTypeBV b v' c tv (NoReftB b))]
-> RTypeBV b v' c tv r -> RTPropBV b v' c tv r
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp (((b, RTypeBV b v c tv (NoReftB b))
 -> (b, RTypeBV b v' c tv (NoReftB b)))
-> [(b, RTypeBV b v c tv (NoReftB b))]
-> [(b, RTypeBV b v' c tv (NoReftB b))]
forall a b. (a -> b) -> [a] -> [b]
map ((RTypeBV b v c tv (NoReftB b) -> RTypeBV b v' c tv (NoReftB b))
-> (b, RTypeBV b v c tv (NoReftB b))
-> (b, RTypeBV b v' c tv (NoReftB b))
forall a b. (a -> b) -> (b, a) -> (b, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((v -> v')
-> RTypeBV b v c tv (NoReftB b) -> RTypeBV b v' c tv (NoReftB b)
forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV v -> v'
f)) [(b, RTypeBV b v c tv (NoReftB b))]
ss) ((v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV v -> v'
f RTypeBV b v c tv r
t)
mapRTypeV v -> v'
f (RAllE b
z RTypeBV b v c tv r
t RTypeBV b v c tv r
t')    = b
-> RTypeBV b v' c tv r
-> RTypeBV b v' c tv r
-> RTypeBV b v' c tv r
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 b
z ((v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV v -> v'
f RTypeBV b v c tv r
t) ((v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV v -> v'
f RTypeBV b v c tv r
t')
mapRTypeV v -> v'
f (REx b
z RTypeBV b v c tv r
t RTypeBV b v c tv r
t')      = b
-> RTypeBV b v' c tv r
-> RTypeBV b v' c tv r
-> RTypeBV b v' c tv r
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 b
z ((v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV v -> v'
f RTypeBV b v c tv r
t) ((v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV v -> v'
f RTypeBV b v c tv r
t')
mapRTypeV v -> v'
f (RExprArg Located (ExprBV b v)
e)      = Located (ExprBV b v') -> RTypeBV b v' c tv r
forall b v c tv r. Located (ExprBV b v) -> RTypeBV b v c tv r
RExprArg ((ExprBV b v -> ExprBV b v')
-> Located (ExprBV b v) -> Located (ExprBV b v')
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((v -> v') -> ExprBV b v -> ExprBV b v'
forall a b. (a -> b) -> ExprBV b a -> ExprBV b b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap v -> v'
f) Located (ExprBV b v)
e)
mapRTypeV v -> v'
f (RAppTy RTypeBV b v c tv r
t RTypeBV b v c tv r
t' r
r)   = RTypeBV b v' c tv r
-> RTypeBV b v' c tv r -> r -> RTypeBV b v' c tv r
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 ((v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV v -> v'
f RTypeBV b v c tv r
t) ((v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV v -> v'
f RTypeBV b v c tv r
t') r
r
mapRTypeV v -> v'
f (RRTy [(b, RTypeBV b v c tv r)]
e r
r Oblig
o RTypeBV b v c tv r
t)    = [(b, RTypeBV b v' c tv r)]
-> r -> Oblig -> RTypeBV b v' c tv r -> RTypeBV b v' c tv r
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 ((RTypeBV b v c tv r -> RTypeBV b v' c tv r)
-> (b, RTypeBV b v c tv r) -> (b, RTypeBV b v' c tv r)
forall a b. (a -> b) -> (b, a) -> (b, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV v -> v'
f) ((b, RTypeBV b v c tv r) -> (b, RTypeBV b v' c tv r))
-> [(b, RTypeBV b v c tv r)] -> [(b, RTypeBV b v' c tv r)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(b, RTypeBV b v c tv r)]
e) r
r Oblig
o ((v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV v -> v'
f RTypeBV b v c tv r
t)
mapRTypeV v -> v'
_ (RHole r
r)         = r -> RTypeBV b v' c tv r
forall b v c tv r. r -> RTypeBV b v c tv r
RHole r
r

mapRTypeVM :: (Hashable b, Monad m) => (v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapRTypeVM :: forall b (m :: * -> *) v v' c tv r.
(Hashable b, Monad m) =>
(v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapRTypeVM v -> m v'
_ (RVar tv
α r
r)        = RTypeBV b v' c tv r -> m (RTypeBV b v' c tv r)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (RTypeBV b v' c tv r -> m (RTypeBV b v' c tv r))
-> RTypeBV b v' c tv r -> m (RTypeBV b v' c tv r)
forall a b. (a -> b) -> a -> b
$ tv -> r -> RTypeBV b v' c tv r
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar tv
α r
r
mapRTypeVM v -> m v'
f (RAllT RTVUBV b v c tv
α RTypeBV b v c tv r
t r
r)     = RTVUBV b v' c tv -> RTypeBV b v' c tv r -> r -> RTypeBV b v' c tv r
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 (RTVUBV b v' c tv
 -> RTypeBV b v' c tv r -> r -> RTypeBV b v' c tv r)
-> m (RTVUBV b v' c tv)
-> m (RTypeBV b v' c tv r -> r -> RTypeBV b v' c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RTypeBV b v c tv (NoReftB b) -> m (RTypeBV b v' c tv (NoReftB b)))
-> RTVUBV b v c tv -> m (RTVUBV b v' c tv)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> RTVar tv a -> f (RTVar tv b)
traverse ((v -> m v')
-> RTypeBV b v c tv (NoReftB b)
-> m (RTypeBV b v' c tv (NoReftB b))
forall b (m :: * -> *) v v' c tv r.
(Hashable b, Monad m) =>
(v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapRTypeVM v -> m v'
f) RTVUBV b v c tv
α m (RTypeBV b v' c tv r -> r -> RTypeBV b v' c tv r)
-> m (RTypeBV b v' c tv r) -> m (r -> RTypeBV b v' c tv r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
forall b (m :: * -> *) v v' c tv r.
(Hashable b, Monad m) =>
(v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapRTypeVM v -> m v'
f RTypeBV b v c tv r
t m (r -> RTypeBV b v' c tv r) -> m r -> m (RTypeBV b v' c tv r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> r -> m r
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure r
r
mapRTypeVM v -> m v'
f (RAllP PVUBV b v c tv
π RTypeBV b v c tv r
t)       = PVUBV b v' c tv -> RTypeBV b v' c tv r -> RTypeBV b v' c tv r
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP (PVUBV b v' c tv -> RTypeBV b v' c tv r -> RTypeBV b v' c tv r)
-> m (PVUBV b v' c tv)
-> m (RTypeBV b v' c tv r -> RTypeBV b v' c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([b] -> v -> m v')
-> ([b]
    -> RTypeBV b v c tv (NoReftB b)
    -> m (RTypeBV b v' c tv (NoReftB b)))
-> PVUBV b v c tv
-> m (PVUBV b v' c tv)
forall (m :: * -> *) b v v' t t'.
(Monad m, Hashable b) =>
([b] -> v -> m v')
-> ([b] -> t -> m t') -> PVarBV b v t -> m (PVarBV b v' t')
emapPVarVM ((v -> m v') -> [b] -> v -> m v'
forall a b. a -> b -> a
const v -> m v'
f) ((RTypeBV b v c tv (NoReftB b) -> m (RTypeBV b v' c tv (NoReftB b)))
-> [b]
-> RTypeBV b v c tv (NoReftB b)
-> m (RTypeBV b v' c tv (NoReftB b))
forall a b. a -> b -> a
const ((v -> m v')
-> RTypeBV b v c tv (NoReftB b)
-> m (RTypeBV b v' c tv (NoReftB b))
forall b (m :: * -> *) v v' c tv r.
(Hashable b, Monad m) =>
(v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapRTypeVM v -> m v'
f)) PVUBV b v c tv
π m (RTypeBV b v' c tv r -> RTypeBV b v' c tv r)
-> m (RTypeBV b v' c tv r) -> m (RTypeBV b v' c tv r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
forall b (m :: * -> *) v v' c tv r.
(Hashable b, Monad m) =>
(v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapRTypeVM v -> m v'
f RTypeBV b v c tv r
t
mapRTypeVM v -> m v'
f (RFun b
x RFInfo
i RTypeBV b v c tv r
t RTypeBV b v c tv r
t' r
r) = b
-> RFInfo
-> RTypeBV b v' c tv r
-> RTypeBV b v' c tv r
-> r
-> RTypeBV b v' c tv r
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 b
x RFInfo
i (RTypeBV b v' c tv r
 -> RTypeBV b v' c tv r -> r -> RTypeBV b v' c tv r)
-> m (RTypeBV b v' c tv r)
-> m (RTypeBV b v' c tv r -> r -> RTypeBV b v' c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
forall b (m :: * -> *) v v' c tv r.
(Hashable b, Monad m) =>
(v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapRTypeVM v -> m v'
f RTypeBV b v c tv r
t m (RTypeBV b v' c tv r -> r -> RTypeBV b v' c tv r)
-> m (RTypeBV b v' c tv r) -> m (r -> RTypeBV b v' c tv r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
forall b (m :: * -> *) v v' c tv r.
(Hashable b, Monad m) =>
(v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapRTypeVM v -> m v'
f RTypeBV b v c tv r
t' m (r -> RTypeBV b v' c tv r) -> m r -> m (RTypeBV b v' c tv r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> r -> m r
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure r
r
mapRTypeVM v -> m v'
f (RApp c
c [RTypeBV b v c tv r]
ts [RTPropBV b v c tv r]
rs r
r)  = c
-> [RTypeBV b v' c tv r]
-> [RTPropBV b v' c tv r]
-> r
-> RTypeBV b v' c tv r
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 c
c ([RTypeBV b v' c tv r]
 -> [RTPropBV b v' c tv r] -> r -> RTypeBV b v' c tv r)
-> m [RTypeBV b v' c tv r]
-> m ([RTPropBV b v' c tv r] -> r -> RTypeBV b v' c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RTypeBV b v c tv r -> m (RTypeBV b v' c tv r))
-> [RTypeBV b v c tv r] -> m [RTypeBV b v' c tv r]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
forall b (m :: * -> *) v v' c tv r.
(Hashable b, Monad m) =>
(v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapRTypeVM v -> m v'
f) [RTypeBV b v c tv r]
ts m ([RTPropBV b v' c tv r] -> r -> RTypeBV b v' c tv r)
-> m [RTPropBV b v' c tv r] -> m (r -> RTypeBV b v' c tv r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (RTPropBV b v c tv r -> m (RTPropBV b v' c tv r))
-> [RTPropBV b v c tv r] -> m [RTPropBV b v' c tv r]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM RTPropBV b v c tv r -> m (RTPropBV b v' c tv r)
mapRefVM [RTPropBV b v c tv r]
rs m (r -> RTypeBV b v' c tv r) -> m r -> m (RTypeBV b v' c tv r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> r -> m r
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure r
r
  where
    mapRefVM :: RTPropBV b v c tv r -> m (RTPropBV b v' c tv r)
mapRefVM (RProp [(b, RTypeBV b v c tv (NoReftB b))]
ss RTypeBV b v c tv r
t) = [(b, RTypeBV b v' c tv (NoReftB b))]
-> RTypeBV b v' c tv r -> RTPropBV b v' c tv r
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp ([(b, RTypeBV b v' c tv (NoReftB b))]
 -> RTypeBV b v' c tv r -> RTPropBV b v' c tv r)
-> m [(b, RTypeBV b v' c tv (NoReftB b))]
-> m (RTypeBV b v' c tv r -> RTPropBV b v' c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((b, RTypeBV b v c tv (NoReftB b))
 -> m (b, RTypeBV b v' c tv (NoReftB b)))
-> [(b, RTypeBV b v c tv (NoReftB b))]
-> m [(b, RTypeBV b v' c tv (NoReftB b))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((RTypeBV b v c tv (NoReftB b) -> m (RTypeBV b v' c tv (NoReftB b)))
-> (b, RTypeBV b v c tv (NoReftB b))
-> m (b, RTypeBV b v' c tv (NoReftB b))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (b, a) -> f (b, b)
traverse ((v -> m v')
-> RTypeBV b v c tv (NoReftB b)
-> m (RTypeBV b v' c tv (NoReftB b))
forall b (m :: * -> *) v v' c tv r.
(Hashable b, Monad m) =>
(v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapRTypeVM v -> m v'
f)) [(b, RTypeBV b v c tv (NoReftB b))]
ss m (RTypeBV b v' c tv r -> RTPropBV b v' c tv r)
-> m (RTypeBV b v' c tv r) -> m (RTPropBV b v' c tv r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
forall b (m :: * -> *) v v' c tv r.
(Hashable b, Monad m) =>
(v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapRTypeVM v -> m v'
f RTypeBV b v c tv r
t
mapRTypeVM v -> m v'
f (RAllE b
z RTypeBV b v c tv r
t RTypeBV b v c tv r
t')    = b
-> RTypeBV b v' c tv r
-> RTypeBV b v' c tv r
-> RTypeBV b v' c tv r
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 b
z (RTypeBV b v' c tv r -> RTypeBV b v' c tv r -> RTypeBV b v' c tv r)
-> m (RTypeBV b v' c tv r)
-> m (RTypeBV b v' c tv r -> RTypeBV b v' c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
forall b (m :: * -> *) v v' c tv r.
(Hashable b, Monad m) =>
(v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapRTypeVM v -> m v'
f RTypeBV b v c tv r
t m (RTypeBV b v' c tv r -> RTypeBV b v' c tv r)
-> m (RTypeBV b v' c tv r) -> m (RTypeBV b v' c tv r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
forall b (m :: * -> *) v v' c tv r.
(Hashable b, Monad m) =>
(v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapRTypeVM v -> m v'
f RTypeBV b v c tv r
t'
mapRTypeVM v -> m v'
f (REx b
z RTypeBV b v c tv r
t RTypeBV b v c tv r
t')      = b
-> RTypeBV b v' c tv r
-> RTypeBV b v' c tv r
-> RTypeBV b v' c tv r
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 b
z (RTypeBV b v' c tv r -> RTypeBV b v' c tv r -> RTypeBV b v' c tv r)
-> m (RTypeBV b v' c tv r)
-> m (RTypeBV b v' c tv r -> RTypeBV b v' c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
forall b (m :: * -> *) v v' c tv r.
(Hashable b, Monad m) =>
(v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapRTypeVM v -> m v'
f RTypeBV b v c tv r
t m (RTypeBV b v' c tv r -> RTypeBV b v' c tv r)
-> m (RTypeBV b v' c tv r) -> m (RTypeBV b v' c tv r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
forall b (m :: * -> *) v v' c tv r.
(Hashable b, Monad m) =>
(v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapRTypeVM v -> m v'
f RTypeBV b v c tv r
t'
mapRTypeVM v -> m v'
f (RExprArg Located (ExprBV b v)
e)      = Located (ExprBV b v') -> RTypeBV b v' c tv r
forall b v c tv r. Located (ExprBV b v) -> RTypeBV b v c tv r
RExprArg (Located (ExprBV b v') -> RTypeBV b v' c tv r)
-> m (Located (ExprBV b v')) -> m (RTypeBV b v' c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ExprBV b v -> m (ExprBV b v'))
-> Located (ExprBV b v) -> m (Located (ExprBV b v'))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Located a -> f (Located b)
traverse ((v -> m v') -> ExprBV b v -> m (ExprBV b v')
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ExprBV b a -> f (ExprBV b b)
traverse v -> m v'
f) Located (ExprBV b v)
e
mapRTypeVM v -> m v'
f (RAppTy RTypeBV b v c tv r
t RTypeBV b v c tv r
t' r
r)   = RTypeBV b v' c tv r
-> RTypeBV b v' c tv r -> r -> RTypeBV b v' c tv r
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 b v' c tv r
 -> RTypeBV b v' c tv r -> r -> RTypeBV b v' c tv r)
-> m (RTypeBV b v' c tv r)
-> m (RTypeBV b v' c tv r -> r -> RTypeBV b v' c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
forall b (m :: * -> *) v v' c tv r.
(Hashable b, Monad m) =>
(v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapRTypeVM v -> m v'
f RTypeBV b v c tv r
t m (RTypeBV b v' c tv r -> r -> RTypeBV b v' c tv r)
-> m (RTypeBV b v' c tv r) -> m (r -> RTypeBV b v' c tv r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
forall b (m :: * -> *) v v' c tv r.
(Hashable b, Monad m) =>
(v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapRTypeVM v -> m v'
f RTypeBV b v c tv r
t' m (r -> RTypeBV b v' c tv r) -> m r -> m (RTypeBV b v' c tv r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> r -> m r
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure r
r
mapRTypeVM v -> m v'
f (RRTy [(b, RTypeBV b v c tv r)]
e r
r Oblig
o RTypeBV b v c tv r
t)    = [(b, RTypeBV b v' c tv r)]
-> r -> Oblig -> RTypeBV b v' c tv r -> RTypeBV b v' c tv r
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 ([(b, RTypeBV b v' c tv r)]
 -> r -> Oblig -> RTypeBV b v' c tv r -> RTypeBV b v' c tv r)
-> m [(b, RTypeBV b v' c tv r)]
-> m (r -> Oblig -> RTypeBV b v' c tv r -> RTypeBV b v' c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((b, RTypeBV b v c tv r) -> m (b, RTypeBV b v' c tv r))
-> [(b, RTypeBV b v c tv r)] -> m [(b, RTypeBV b v' c tv r)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((RTypeBV b v c tv r -> m (RTypeBV b v' c tv r))
-> (b, RTypeBV b v c tv r) -> m (b, RTypeBV b v' c tv r)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (b, a) -> f (b, b)
traverse ((v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
forall b (m :: * -> *) v v' c tv r.
(Hashable b, Monad m) =>
(v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapRTypeVM v -> m v'
f)) [(b, RTypeBV b v c tv r)]
e m (r -> Oblig -> RTypeBV b v' c tv r -> RTypeBV b v' c tv r)
-> m r -> m (Oblig -> RTypeBV b v' c tv r -> RTypeBV b v' c tv r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> r -> m r
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure r
r m (Oblig -> RTypeBV b v' c tv r -> RTypeBV b v' c tv r)
-> m Oblig -> m (RTypeBV b v' c tv r -> RTypeBV b v' c tv r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Oblig -> m Oblig
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Oblig
o m (RTypeBV b v' c tv r -> RTypeBV b v' c tv r)
-> m (RTypeBV b v' c tv r) -> m (RTypeBV b v' c tv r)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
forall b (m :: * -> *) v v' c tv r.
(Hashable b, Monad m) =>
(v -> m v') -> RTypeBV b v c tv r -> m (RTypeBV b v' c tv r)
mapRTypeVM v -> m v'
f RTypeBV b v c tv r
t
mapRTypeVM v -> m v'
_ (RHole r
r)         = RTypeBV b v' c tv r -> m (RTypeBV b v' c tv r)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (r -> RTypeBV b v' c tv r
forall b v c tv r. r -> RTypeBV b v c tv r
RHole r
r)

emapFReftM :: Monad m => ([Symbol] -> v -> m v') -> F.ReftV v -> m (F.ReftV v')
emapFReftM :: forall (m :: * -> *) v v'.
Monad m =>
([Symbol] -> v -> m v') -> ReftV v -> m (ReftV v')
emapFReftM [Symbol] -> v -> m v'
f (F.Reft (Symbol
v, ExprBV Symbol v
e)) = Symbol -> ExprV v' -> ReftV v'
forall v. Symbol -> ExprV v -> ReftV v
F.reft Symbol
v (ExprV v' -> ReftV v') -> m (ExprV v') -> m (ReftV v')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Symbol] -> v -> m v') -> ExprBV Symbol v -> m (ExprV v')
forall (m :: * -> *) b v v'.
(Monad m, Hashable b) =>
([b] -> v -> m v') -> ExprBV b v -> m (ExprBV b v')
emapExprVM ([Symbol] -> v -> m v'
f ([Symbol] -> v -> m v')
-> ([Symbol] -> [Symbol]) -> [Symbol] -> v -> m v'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol
vSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:)) ExprBV Symbol v
e

-- The first parameter corresponds to the bscope config setting
emapReftM
  :: (Monad m, ToReft r1, F.Binder b, CompatibleBinder b tv, ReftBind r1 ~ b)
  => Bool
  -> ([b] -> v1 -> m v2)
  -> ([b] -> r1 -> m r2)
  -> [b]
  -> RTypeBV b v1 c tv r1
  -> m (RTypeBV b v2 c tv r2)
emapReftM :: forall (m :: * -> *) r1 b tv v1 v2 r2 c.
(Monad m, ToReft r1, Binder b, CompatibleBinder b tv,
 ReftBind r1 ~ b) =>
Bool
-> ([b] -> v1 -> m v2)
-> ([b] -> r1 -> m r2)
-> [b]
-> RTypeBV b v1 c tv r1
-> m (RTypeBV b v2 c tv r2)
emapReftM Bool
bscp [b] -> v1 -> m v2
vf [b] -> r1 -> m r2
f = [b] -> RTypeBV b v1 c tv r1 -> m (RTypeBV b v2 c tv r2)
go
  where
    go :: [b] -> RTypeBV b v1 c tv r1 -> m (RTypeBV b v2 c tv r2)
go [b]
γ (RVar tv
α r1
r)        = tv -> r2 -> RTypeBV b v2 c tv r2
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar  tv
α (r2 -> RTypeBV b v2 c tv r2) -> m r2 -> m (RTypeBV b v2 c tv r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [b] -> r1 -> m r2
f [b]
γ r1
r
    go [b]
γ (RAllT RTVUBV b v1 c tv
α RTypeBV b v1 c tv r1
t r1
r)     = RTVUBV b v2 c tv
-> RTypeBV b v2 c tv r2 -> r2 -> RTypeBV b v2 c tv r2
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 (RTVUBV b v2 c tv
 -> RTypeBV b v2 c tv r2 -> r2 -> RTypeBV b v2 c tv r2)
-> m (RTVUBV b v2 c tv)
-> m (RTypeBV b v2 c tv r2 -> r2 -> RTypeBV b v2 c tv r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RTypeBV b v1 c tv (NoReftB b)
 -> m (RTypeBV b v2 c tv (NoReftB b)))
-> RTVUBV b v1 c tv -> m (RTVUBV b v2 c tv)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> RTVar tv a -> f (RTVar tv b)
traverse (Bool
-> ([b] -> v1 -> m v2)
-> ([b] -> NoReftB b -> m (NoReftB b))
-> [b]
-> RTypeBV b v1 c tv (NoReftB b)
-> m (RTypeBV b v2 c tv (NoReftB b))
forall (m :: * -> *) r1 b tv v1 v2 r2 c.
(Monad m, ToReft r1, Binder b, CompatibleBinder b tv,
 ReftBind r1 ~ b) =>
Bool
-> ([b] -> v1 -> m v2)
-> ([b] -> r1 -> m r2)
-> [b]
-> RTypeBV b v1 c tv r1
-> m (RTypeBV b v2 c tv r2)
emapReftM Bool
bscp [b] -> v1 -> m v2
vf ((NoReftB b -> m (NoReftB b)) -> [b] -> NoReftB b -> m (NoReftB b)
forall a b. a -> b -> a
const NoReftB b -> m (NoReftB b)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure) [b]
γ) RTVUBV b v1 c tv
α m (RTypeBV b v2 c tv r2 -> r2 -> RTypeBV b v2 c tv r2)
-> m (RTypeBV b v2 c tv r2) -> m (r2 -> RTypeBV b v2 c tv r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [b] -> RTypeBV b v1 c tv r1 -> m (RTypeBV b v2 c tv r2)
go (tv -> b
forall b b'. CompatibleBinder b b' => b' -> b
coerceBinder (RTVUBV b v1 c tv -> tv
forall tv s. RTVar tv s -> tv
ty_var_value RTVUBV b v1 c tv
α) b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b]
γ) RTypeBV b v1 c tv r1
t m (r2 -> RTypeBV b v2 c tv r2) -> m r2 -> m (RTypeBV b v2 c tv r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [b] -> r1 -> m r2
f [b]
γ r1
r
    go [b]
γ (RAllP PVUBV b v1 c tv
π RTypeBV b v1 c tv r1
t)       = PVUBV b v2 c tv -> RTypeBV b v2 c tv r2 -> RTypeBV b v2 c tv r2
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP (PVUBV b v2 c tv -> RTypeBV b v2 c tv r2 -> RTypeBV b v2 c tv r2)
-> m (PVUBV b v2 c tv)
-> m (RTypeBV b v2 c tv r2 -> RTypeBV b v2 c tv r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([b] -> v1 -> m v2)
-> ([b]
    -> RTypeBV b v1 c tv (NoReftB b)
    -> m (RTypeBV b v2 c tv (NoReftB b)))
-> PVUBV b v1 c tv
-> m (PVUBV b v2 c tv)
forall (m :: * -> *) b v v' t t'.
(Monad m, Hashable b) =>
([b] -> v -> m v')
-> ([b] -> t -> m t') -> PVarBV b v t -> m (PVarBV b v' t')
emapPVarVM [b] -> v1 -> m v2
vf (Bool
-> ([b] -> v1 -> m v2)
-> ([b] -> NoReftB b -> m (NoReftB b))
-> [b]
-> RTypeBV b v1 c tv (NoReftB b)
-> m (RTypeBV b v2 c tv (NoReftB b))
forall (m :: * -> *) r1 b tv v1 v2 r2 c.
(Monad m, ToReft r1, Binder b, CompatibleBinder b tv,
 ReftBind r1 ~ b) =>
Bool
-> ([b] -> v1 -> m v2)
-> ([b] -> r1 -> m r2)
-> [b]
-> RTypeBV b v1 c tv r1
-> m (RTypeBV b v2 c tv r2)
emapReftM Bool
bscp [b] -> v1 -> m v2
vf ((NoReftB b -> m (NoReftB b)) -> [b] -> NoReftB b -> m (NoReftB b)
forall a b. a -> b -> a
const NoReftB b -> m (NoReftB b)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure)) PVUBV b v1 c tv
π m (RTypeBV b v2 c tv r2 -> RTypeBV b v2 c tv r2)
-> m (RTypeBV b v2 c tv r2) -> m (RTypeBV b v2 c tv r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [b] -> RTypeBV b v1 c tv r1 -> m (RTypeBV b v2 c tv r2)
go [b]
γ RTypeBV b v1 c tv r1
t
    go [b]
γ (RFun b
x RFInfo
i RTypeBV b v1 c tv r1
t RTypeBV b v1 c tv r1
t' r1
r) = b
-> RFInfo
-> RTypeBV b v2 c tv r2
-> RTypeBV b v2 c tv r2
-> r2
-> RTypeBV b v2 c tv r2
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  b
x RFInfo
i (RTypeBV b v2 c tv r2
 -> RTypeBV b v2 c tv r2 -> r2 -> RTypeBV b v2 c tv r2)
-> m (RTypeBV b v2 c tv r2)
-> m (RTypeBV b v2 c tv r2 -> r2 -> RTypeBV b v2 c tv r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [b] -> RTypeBV b v1 c tv r1 -> m (RTypeBV b v2 c tv r2)
go (b
xb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
γ) RTypeBV b v1 c tv r1
t m (RTypeBV b v2 c tv r2 -> r2 -> RTypeBV b v2 c tv r2)
-> m (RTypeBV b v2 c tv r2) -> m (r2 -> RTypeBV b v2 c tv r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [b] -> RTypeBV b v1 c tv r1 -> m (RTypeBV b v2 c tv r2)
go (b
xb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
γ) RTypeBV b v1 c tv r1
t' m (r2 -> RTypeBV b v2 c tv r2) -> m r2 -> m (RTypeBV b v2 c tv r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [b] -> r1 -> m r2
f (b
xb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
γ) r1
r
    go [b]
γ (RApp c
c [RTypeBV b v1 c tv r1]
ts [RTPropBV b v1 c tv r1]
rs r1
r)  =
      let γ' :: [b]
γ' = if Bool
bscp then ReftBV b (ReftVar r1) -> b
forall b v. ReftBV b v -> b
F.reftBind (r1 -> ReftBV (ReftBind r1) (ReftVar r1)
forall r. ToReft r => r -> ReftBV (ReftBind r) (ReftVar r)
toReft r1
r) b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b]
γ  else [b]
γ
       in c
-> [RTypeBV b v2 c tv r2]
-> [RTPropBV b v2 c tv r2]
-> r2
-> RTypeBV b v2 c tv r2
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  c
c ([RTypeBV b v2 c tv r2]
 -> [RTPropBV b v2 c tv r2] -> r2 -> RTypeBV b v2 c tv r2)
-> m [RTypeBV b v2 c tv r2]
-> m ([RTPropBV b v2 c tv r2] -> r2 -> RTypeBV b v2 c tv r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RTypeBV b v1 c tv r1 -> m (RTypeBV b v2 c tv r2))
-> [RTypeBV b v1 c tv r1] -> m [RTypeBV b v2 c tv r2]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([b] -> RTypeBV b v1 c tv r1 -> m (RTypeBV b v2 c tv r2)
go [b]
γ') [RTypeBV b v1 c tv r1]
ts m ([RTPropBV b v2 c tv r2] -> r2 -> RTypeBV b v2 c tv r2)
-> m [RTPropBV b v2 c tv r2] -> m (r2 -> RTypeBV b v2 c tv r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (RTPropBV b v1 c tv r1 -> m (RTPropBV b v2 c tv r2))
-> [RTPropBV b v1 c tv r1] -> m [RTPropBV b v2 c tv r2]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Bool
-> ([b] -> v1 -> m v2)
-> ([b] -> r1 -> m r2)
-> [b]
-> RTPropBV b v1 c tv r1
-> m (RTPropBV b v2 c tv r2)
forall (m :: * -> *) t b tv v v' s c.
(Monad m, ToReft t, Binder b, CompatibleBinder b tv,
 ReftBind t ~ b) =>
Bool
-> ([b] -> v -> m v')
-> ([b] -> t -> m s)
-> [b]
-> RTPropBV b v c tv t
-> m (RTPropBV b v' c tv s)
emapRefM Bool
bscp [b] -> v1 -> m v2
vf [b] -> r1 -> m r2
f [b]
γ) [RTPropBV b v1 c tv r1]
rs m (r2 -> RTypeBV b v2 c tv r2) -> m r2 -> m (RTypeBV b v2 c tv r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [b] -> r1 -> m r2
f [b]
γ r1
r
    go [b]
γ (RAllE b
z RTypeBV b v1 c tv r1
t RTypeBV b v1 c tv r1
t')    = b
-> RTypeBV b v2 c tv r2
-> RTypeBV b v2 c tv r2
-> RTypeBV b v2 c tv r2
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 b
z (RTypeBV b v2 c tv r2
 -> RTypeBV b v2 c tv r2 -> RTypeBV b v2 c tv r2)
-> m (RTypeBV b v2 c tv r2)
-> m (RTypeBV b v2 c tv r2 -> RTypeBV b v2 c tv r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [b] -> RTypeBV b v1 c tv r1 -> m (RTypeBV b v2 c tv r2)
go [b]
γ RTypeBV b v1 c tv r1
t m (RTypeBV b v2 c tv r2 -> RTypeBV b v2 c tv r2)
-> m (RTypeBV b v2 c tv r2) -> m (RTypeBV b v2 c tv r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [b] -> RTypeBV b v1 c tv r1 -> m (RTypeBV b v2 c tv r2)
go [b]
γ RTypeBV b v1 c tv r1
t'
    go [b]
γ (REx b
z RTypeBV b v1 c tv r1
t RTypeBV b v1 c tv r1
t')      = b
-> RTypeBV b v2 c tv r2
-> RTypeBV b v2 c tv r2
-> RTypeBV b v2 c tv r2
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   b
z (RTypeBV b v2 c tv r2
 -> RTypeBV b v2 c tv r2 -> RTypeBV b v2 c tv r2)
-> m (RTypeBV b v2 c tv r2)
-> m (RTypeBV b v2 c tv r2 -> RTypeBV b v2 c tv r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [b] -> RTypeBV b v1 c tv r1 -> m (RTypeBV b v2 c tv r2)
go [b]
γ RTypeBV b v1 c tv r1
t m (RTypeBV b v2 c tv r2 -> RTypeBV b v2 c tv r2)
-> m (RTypeBV b v2 c tv r2) -> m (RTypeBV b v2 c tv r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [b] -> RTypeBV b v1 c tv r1 -> m (RTypeBV b v2 c tv r2)
go [b]
γ RTypeBV b v1 c tv r1
t'
    go [b]
γ (RExprArg Located (ExprBV b v1)
e)      = Located (ExprBV b v2) -> RTypeBV b v2 c tv r2
forall b v c tv r. Located (ExprBV b v) -> RTypeBV b v c tv r
RExprArg (Located (ExprBV b v2) -> RTypeBV b v2 c tv r2)
-> m (Located (ExprBV b v2)) -> m (RTypeBV b v2 c tv r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ExprBV b v1 -> m (ExprBV b v2))
-> Located (ExprBV b v1) -> m (Located (ExprBV b v2))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Located a -> f (Located b)
traverse (([b] -> v1 -> m v2) -> ExprBV b v1 -> m (ExprBV b v2)
forall (m :: * -> *) b v v'.
(Monad m, Hashable b) =>
([b] -> v -> m v') -> ExprBV b v -> m (ExprBV b v')
emapExprVM ([b] -> v1 -> m v2
vf ([b] -> v1 -> m v2) -> ([b] -> [b]) -> [b] -> v1 -> m v2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++[b]
γ))) Located (ExprBV b v1)
e
    go [b]
γ (RAppTy RTypeBV b v1 c tv r1
t RTypeBV b v1 c tv r1
t' r1
r)   = RTypeBV b v2 c tv r2
-> RTypeBV b v2 c tv r2 -> r2 -> RTypeBV b v2 c tv r2
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 b v2 c tv r2
 -> RTypeBV b v2 c tv r2 -> r2 -> RTypeBV b v2 c tv r2)
-> m (RTypeBV b v2 c tv r2)
-> m (RTypeBV b v2 c tv r2 -> r2 -> RTypeBV b v2 c tv r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [b] -> RTypeBV b v1 c tv r1 -> m (RTypeBV b v2 c tv r2)
go [b]
γ RTypeBV b v1 c tv r1
t m (RTypeBV b v2 c tv r2 -> r2 -> RTypeBV b v2 c tv r2)
-> m (RTypeBV b v2 c tv r2) -> m (r2 -> RTypeBV b v2 c tv r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [b] -> RTypeBV b v1 c tv r1 -> m (RTypeBV b v2 c tv r2)
go [b]
γ RTypeBV b v1 c tv r1
t' m (r2 -> RTypeBV b v2 c tv r2) -> m r2 -> m (RTypeBV b v2 c tv r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [b] -> r1 -> m r2
f [b]
γ r1
r
    go [b]
γ (RRTy [(b, RTypeBV b v1 c tv r1)]
e r1
r Oblig
o RTypeBV b v1 c tv r1
t)    =
      [(b, RTypeBV b v2 c tv r2)]
-> r2 -> Oblig -> RTypeBV b v2 c tv r2 -> RTypeBV b v2 c tv r2
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 ([(b, RTypeBV b v2 c tv r2)]
 -> r2 -> Oblig -> RTypeBV b v2 c tv r2 -> RTypeBV b v2 c tv r2)
-> m [(b, RTypeBV b v2 c tv r2)]
-> m (r2 -> Oblig -> RTypeBV b v2 c tv r2 -> RTypeBV b v2 c tv r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((b, RTypeBV b v1 c tv r1) -> m (b, RTypeBV b v2 c tv r2))
-> [(b, RTypeBV b v1 c tv r1)] -> m [(b, RTypeBV b v2 c tv r2)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((RTypeBV b v1 c tv r1 -> m (RTypeBV b v2 c tv r2))
-> (b, RTypeBV b v1 c tv r1) -> m (b, RTypeBV b v2 c tv r2)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (b, a) -> f (b, b)
traverse ([b] -> RTypeBV b v1 c tv r1 -> m (RTypeBV b v2 c tv r2)
go (((b, RTypeBV b v1 c tv r1) -> b)
-> [(b, RTypeBV b v1 c tv r1)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (b, RTypeBV b v1 c tv r1) -> b
forall a b. (a, b) -> a
fst [(b, RTypeBV b v1 c tv r1)]
e [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++ [b]
γ))) [(b, RTypeBV b v1 c tv r1)]
e m (r2 -> Oblig -> RTypeBV b v2 c tv r2 -> RTypeBV b v2 c tv r2)
-> m r2
-> m (Oblig -> RTypeBV b v2 c tv r2 -> RTypeBV b v2 c tv r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [b] -> r1 -> m r2
f [b]
γ r1
r m (Oblig -> RTypeBV b v2 c tv r2 -> RTypeBV b v2 c tv r2)
-> m Oblig -> m (RTypeBV b v2 c tv r2 -> RTypeBV b v2 c tv r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Oblig -> m Oblig
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Oblig
o m (RTypeBV b v2 c tv r2 -> RTypeBV b v2 c tv r2)
-> m (RTypeBV b v2 c tv r2) -> m (RTypeBV b v2 c tv r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [b] -> RTypeBV b v1 c tv r1 -> m (RTypeBV b v2 c tv r2)
go [b]
γ RTypeBV b v1 c tv r1
t
    go [b]
γ (RHole r1
r)         = r2 -> RTypeBV b v2 c tv r2
forall b v c tv r. r -> RTypeBV b v c tv r
RHole (r2 -> RTypeBV b v2 c tv r2) -> m r2 -> m (RTypeBV b v2 c tv r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [b] -> r1 -> m r2
f [b]
γ r1
r

emapRefM
  :: (Monad m, ToReft t, F.Binder b, CompatibleBinder b tv, ReftBind t ~ b)
  => Bool
  -> ([b] -> v -> m v')
  -> ([b] -> t -> m s)
  -> [b]
  -> RTPropBV b v c tv t
  -> m (RTPropBV b v' c tv s)
emapRefM :: forall (m :: * -> *) t b tv v v' s c.
(Monad m, ToReft t, Binder b, CompatibleBinder b tv,
 ReftBind t ~ b) =>
Bool
-> ([b] -> v -> m v')
-> ([b] -> t -> m s)
-> [b]
-> RTPropBV b v c tv t
-> m (RTPropBV b v' c tv s)
emapRefM Bool
bscp [b] -> v -> m v'
vf [b] -> t -> m s
f [b]
γ0 (RProp [(b, RTypeBV b v c tv (NoReftB b))]
ss RTypeBV b v c tv t
t0) =
    [(b, RTypeBV b v' c tv (NoReftB b))]
-> RTypeBV b v' c tv s
-> RefB b (RTypeBV b v' c tv (NoReftB b)) (RTypeBV b v' c tv s)
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp ([(b, RTypeBV b v' c tv (NoReftB b))]
 -> RTypeBV b v' c tv s
 -> RefB b (RTypeBV b v' c tv (NoReftB b)) (RTypeBV b v' c tv s))
-> (([b], [(b, RTypeBV b v' c tv (NoReftB b))])
    -> [(b, RTypeBV b v' c tv (NoReftB b))])
-> ([b], [(b, RTypeBV b v' c tv (NoReftB b))])
-> RTypeBV b v' c tv s
-> RefB b (RTypeBV b v' c tv (NoReftB b)) (RTypeBV b v' c tv s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([b], [(b, RTypeBV b v' c tv (NoReftB b))])
-> [(b, RTypeBV b v' c tv (NoReftB b))]
forall a b. (a, b) -> b
snd (([b], [(b, RTypeBV b v' c tv (NoReftB b))])
 -> RTypeBV b v' c tv s
 -> RefB b (RTypeBV b v' c tv (NoReftB b)) (RTypeBV b v' c tv s))
-> m ([b], [(b, RTypeBV b v' c tv (NoReftB b))])
-> m (RTypeBV b v' c tv s
      -> RefB b (RTypeBV b v' c tv (NoReftB b)) (RTypeBV b v' c tv s))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      ([b]
 -> (b, RTypeBV b v c tv (NoReftB b))
 -> m ([b], (b, RTypeBV b v' c tv (NoReftB b))))
-> [b]
-> [(b, RTypeBV b v c tv (NoReftB b))]
-> m ([b], [(b, RTypeBV b v' c tv (NoReftB b))])
forall (m :: * -> *) (t :: * -> *) a b c.
(Monad m, Traversable t) =>
(a -> b -> m (a, c)) -> a -> t b -> m (a, t c)
mapAccumM
        (\[b]
γ (b
s, RTypeBV b v c tv (NoReftB b)
t) -> (b
sb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
γ,) ((b, RTypeBV b v' c tv (NoReftB b))
 -> ([b], (b, RTypeBV b v' c tv (NoReftB b))))
-> (RTypeBV b v' c tv (NoReftB b)
    -> (b, RTypeBV b v' c tv (NoReftB b)))
-> RTypeBV b v' c tv (NoReftB b)
-> ([b], (b, RTypeBV b v' c tv (NoReftB b)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b
s,) (RTypeBV b v' c tv (NoReftB b)
 -> ([b], (b, RTypeBV b v' c tv (NoReftB b))))
-> m (RTypeBV b v' c tv (NoReftB b))
-> m ([b], (b, RTypeBV b v' c tv (NoReftB b)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> ([b] -> v -> m v')
-> ([b] -> NoReftB b -> m (NoReftB b))
-> [b]
-> RTypeBV b v c tv (NoReftB b)
-> m (RTypeBV b v' c tv (NoReftB b))
forall (m :: * -> *) r1 b tv v1 v2 r2 c.
(Monad m, ToReft r1, Binder b, CompatibleBinder b tv,
 ReftBind r1 ~ b) =>
Bool
-> ([b] -> v1 -> m v2)
-> ([b] -> r1 -> m r2)
-> [b]
-> RTypeBV b v1 c tv r1
-> m (RTypeBV b v2 c tv r2)
emapReftM Bool
bscp [b] -> v -> m v'
vf ((NoReftB b -> m (NoReftB b)) -> [b] -> NoReftB b -> m (NoReftB b)
forall a b. a -> b -> a
const NoReftB b -> m (NoReftB b)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure) [b]
γ RTypeBV b v c tv (NoReftB b)
t)
        [b]
γ0
        [(b, RTypeBV b v c tv (NoReftB b))]
ss
      m (RTypeBV b v' c tv s
   -> RefB b (RTypeBV b v' c tv (NoReftB b)) (RTypeBV b v' c tv s))
-> m (RTypeBV b v' c tv s)
-> m (RefB b (RTypeBV b v' c tv (NoReftB b)) (RTypeBV b v' c tv s))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool
-> ([b] -> v -> m v')
-> ([b] -> t -> m s)
-> [b]
-> RTypeBV b v c tv t
-> m (RTypeBV b v' c tv s)
forall (m :: * -> *) r1 b tv v1 v2 r2 c.
(Monad m, ToReft r1, Binder b, CompatibleBinder b tv,
 ReftBind r1 ~ b) =>
Bool
-> ([b] -> v1 -> m v2)
-> ([b] -> r1 -> m r2)
-> [b]
-> RTypeBV b v1 c tv r1
-> m (RTypeBV b v2 c tv r2)
emapReftM Bool
bscp [b] -> v -> m v'
vf [b] -> t -> m s
f (((b, RTypeBV b v c tv (NoReftB b)) -> b)
-> [(b, RTypeBV b v c tv (NoReftB b))] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (b, RTypeBV b v c tv (NoReftB b)) -> b
forall a b. (a, b) -> a
fst [(b, RTypeBV b v c tv (NoReftB b))]
ss [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++ [b]
γ0) RTypeBV b v c tv t
t0

emapBareTypeVM
  :: (Monad m, Ord v1)
  => Bool
  -> ([Symbol] -> v1 -> m v2)
  -> [Symbol]
  -> BareTypeV v1
  -> m (BareTypeV v2)
emapBareTypeVM :: forall (m :: * -> *) v1 v2.
(Monad m, Ord v1) =>
Bool
-> ([Symbol] -> v1 -> m v2)
-> [Symbol]
-> BareTypeV v1
-> m (BareTypeV v2)
emapBareTypeVM Bool
bscp [Symbol] -> v1 -> m v2
f =
    Bool
-> ([Symbol] -> v1 -> m v2)
-> ([Symbol] -> RReftV v1 -> m (RReftV v2))
-> [Symbol]
-> RTypeBV Symbol v1 BTyCon BTyVar (RReftV v1)
-> m (RTypeBV Symbol v2 BTyCon BTyVar (RReftV v2))
forall (m :: * -> *) r1 b tv v1 v2 r2 c.
(Monad m, ToReft r1, Binder b, CompatibleBinder b tv,
 ReftBind r1 ~ b) =>
Bool
-> ([b] -> v1 -> m v2)
-> ([b] -> r1 -> m r2)
-> [b]
-> RTypeBV b v1 c tv r1
-> m (RTypeBV b v2 c tv r2)
emapReftM
      Bool
bscp
      [Symbol] -> v1 -> m v2
f
      (\[Symbol]
e -> ([Symbol] -> v1 -> m v2)
-> (ReftBV Symbol v1 -> m (ReftBV Symbol v2))
-> RReftV v1
-> m (RReftV v2)
forall (m :: * -> *) v v' r r'.
Monad m =>
([Symbol] -> v -> m v')
-> (r -> m r') -> UReftV v r -> m (UReftV v' r')
emapUReftVM ([Symbol] -> v1 -> m v2
f ([Symbol] -> v1 -> m v2)
-> ([Symbol] -> [Symbol]) -> [Symbol] -> v1 -> m v2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
e)) (([Symbol] -> v1 -> m v2)
-> ReftBV Symbol v1 -> m (ReftBV Symbol v2)
forall (m :: * -> *) v v'.
Monad m =>
([Symbol] -> v -> m v') -> ReftV v -> m (ReftV v')
emapFReftM ([Symbol] -> v1 -> m v2
f ([Symbol] -> v1 -> m v2)
-> ([Symbol] -> [Symbol]) -> [Symbol] -> v1 -> m v2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
e))))

mapDataDeclV :: (v -> v') -> DataDeclP v ty -> DataDeclP v' ty
mapDataDeclV :: forall v v' ty. (v -> v') -> DataDeclP v ty -> DataDeclP v' ty
mapDataDeclV v -> v'
f DataDecl {[Symbol]
[PVarV v (BSortV v)]
Maybe ty
Maybe [DataCtorP ty]
Maybe (SizeFunV v)
SourcePos
DataDeclKind
DataName
tycName :: DataName
tycTyVars :: [Symbol]
tycPVars :: [PVarV v (BSortV v)]
tycDCons :: Maybe [DataCtorP ty]
tycSrcPos :: SourcePos
tycSFun :: Maybe (SizeFunV v)
tycPropTy :: Maybe ty
tycKind :: DataDeclKind
tycKind :: forall v ty. DataDeclP v ty -> DataDeclKind
tycPropTy :: forall v ty. DataDeclP v ty -> Maybe ty
tycSFun :: forall v ty. DataDeclP v ty -> Maybe (SizeFunV v)
tycSrcPos :: forall v ty. DataDeclP v ty -> SourcePos
tycDCons :: forall v ty. DataDeclP v ty -> Maybe [DataCtorP ty]
tycPVars :: forall v ty. DataDeclP v ty -> [PVarV v (BSortV v)]
tycTyVars :: forall v ty. DataDeclP v ty -> [Symbol]
tycName :: forall v ty. DataDeclP v ty -> DataName
..} =
    DataDecl
      { tycPVars :: [PVarV v' (BSortV v')]
tycPVars = (PVarV v (BSortV v) -> PVarV v' (BSortV v'))
-> [PVarV v (BSortV v)] -> [PVarV v' (BSortV v')]
forall a b. (a -> b) -> [a] -> [b]
map ((v -> v')
-> (BSortV v -> BSortV v')
-> PVarV v (BSortV v)
-> PVarV v' (BSortV v')
forall v v' t t' b.
(v -> v') -> (t -> t') -> PVarBV b v t -> PVarBV b v' t'
mapPVarV v -> v'
f ((v -> v') -> BSortV v -> BSortV v'
forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV v -> v'
f)) [PVarV v (BSortV v)]
tycPVars
      , tycSFun :: Maybe (SizeFunV v')
tycSFun = (SizeFunV v -> SizeFunV v')
-> Maybe (SizeFunV v) -> Maybe (SizeFunV v')
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((v -> v') -> SizeFunV v -> SizeFunV v'
forall a b. (a -> b) -> SizeFunV a -> SizeFunV b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap v -> v'
f) Maybe (SizeFunV v)
tycSFun
      , [Symbol]
Maybe ty
Maybe [DataCtorP ty]
SourcePos
DataDeclKind
DataName
tycName :: DataName
tycTyVars :: [Symbol]
tycDCons :: Maybe [DataCtorP ty]
tycSrcPos :: SourcePos
tycPropTy :: Maybe ty
tycKind :: DataDeclKind
tycKind :: DataDeclKind
tycPropTy :: Maybe ty
tycSrcPos :: SourcePos
tycDCons :: Maybe [DataCtorP ty]
tycTyVars :: [Symbol]
tycName :: DataName
..
      }

mapDataDeclVM :: Monad m => (v -> m v') -> DataDeclP v ty -> m (DataDeclP v' ty)
mapDataDeclVM :: forall (m :: * -> *) v v' ty.
Monad m =>
(v -> m v') -> DataDeclP v ty -> m (DataDeclP v' ty)
mapDataDeclVM v -> m v'
f = Bool
-> ([Symbol] -> v -> m v')
-> ([Symbol] -> ty -> m ty)
-> DataDeclP v ty
-> m (DataDeclP v' ty)
forall (m :: * -> *) v v' ty ty'.
Monad m =>
Bool
-> ([Symbol] -> v -> m v')
-> ([Symbol] -> ty -> m ty')
-> DataDeclP v ty
-> m (DataDeclP v' ty')
emapDataDeclM Bool
False ((v -> m v') -> [Symbol] -> v -> m v'
forall a b. a -> b -> a
const v -> m v'
f) ((ty -> m ty) -> [Symbol] -> ty -> m ty
forall a b. a -> b -> a
const ty -> m ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure)

emapDataDeclM
  :: Monad m
  => Bool
  -> ([Symbol] -> v -> m v')
  -> ([Symbol] -> ty -> m ty')
  -> DataDeclP v ty
  -> m (DataDeclP v' ty')
emapDataDeclM :: forall (m :: * -> *) v v' ty ty'.
Monad m =>
Bool
-> ([Symbol] -> v -> m v')
-> ([Symbol] -> ty -> m ty')
-> DataDeclP v ty
-> m (DataDeclP v' ty')
emapDataDeclM Bool
bscp [Symbol] -> v -> m v'
vf [Symbol] -> ty -> m ty'
f DataDeclP v ty
d = do
    tycPVars <- (PVarBV Symbol v (RTypeBV Symbol v BTyCon BTyVar (NoReftB Symbol))
 -> m (PVarBV
         Symbol v' (RTypeBV Symbol v' BTyCon BTyVar (NoReftB Symbol))))
-> [PVarBV
      Symbol v (RTypeBV Symbol v BTyCon BTyVar (NoReftB Symbol))]
-> m [PVarBV
        Symbol v' (RTypeBV Symbol v' BTyCon BTyVar (NoReftB Symbol))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (([Symbol] -> v -> m v')
-> ([Symbol]
    -> RTypeBV Symbol v BTyCon BTyVar (NoReftB Symbol)
    -> m (RTypeBV Symbol v' BTyCon BTyVar (NoReftB Symbol)))
-> PVarBV
     Symbol v (RTypeBV Symbol v BTyCon BTyVar (NoReftB Symbol))
-> m (PVarBV
        Symbol v' (RTypeBV Symbol v' BTyCon BTyVar (NoReftB Symbol)))
forall (m :: * -> *) b v v' t t'.
(Monad m, Hashable b) =>
([b] -> v -> m v')
-> ([b] -> t -> m t') -> PVarBV b v t -> m (PVarBV b v' t')
emapPVarVM [Symbol] -> v -> m v'
vf (Bool
-> ([Symbol] -> v -> m v')
-> ([Symbol] -> NoReftB Symbol -> m (NoReftB Symbol))
-> [Symbol]
-> RTypeBV Symbol v BTyCon BTyVar (NoReftB Symbol)
-> m (RTypeBV Symbol v' BTyCon BTyVar (NoReftB Symbol))
forall (m :: * -> *) r1 b tv v1 v2 r2 c.
(Monad m, ToReft r1, Binder b, CompatibleBinder b tv,
 ReftBind r1 ~ b) =>
Bool
-> ([b] -> v1 -> m v2)
-> ([b] -> r1 -> m r2)
-> [b]
-> RTypeBV b v1 c tv r1
-> m (RTypeBV b v2 c tv r2)
emapReftM Bool
bscp [Symbol] -> v -> m v'
vf ((NoReftB Symbol -> m (NoReftB Symbol))
-> [Symbol] -> NoReftB Symbol -> m (NoReftB Symbol)
forall a b. a -> b -> a
const NoReftB Symbol -> m (NoReftB Symbol)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure))) ([PVarBV
    Symbol v (RTypeBV Symbol v BTyCon BTyVar (NoReftB Symbol))]
 -> m [PVarBV
         Symbol v' (RTypeBV Symbol v' BTyCon BTyVar (NoReftB Symbol))])
-> [PVarBV
      Symbol v (RTypeBV Symbol v BTyCon BTyVar (NoReftB Symbol))]
-> m [PVarBV
        Symbol v' (RTypeBV Symbol v' BTyCon BTyVar (NoReftB Symbol))]
forall a b. (a -> b) -> a -> b
$ DataDeclP v ty
-> [PVarBV
      Symbol v (RTypeBV Symbol v BTyCon BTyVar (NoReftB Symbol))]
forall v ty. DataDeclP v ty -> [PVarV v (BSortV v)]
tycPVars DataDeclP v ty
d
    tycDCons <- traverse (mapM (emapDataCtorTyM f)) (tycDCons d)
    tycSFun <- traverse (traverse (vf [])) (tycSFun d)
    tycPropTy <- traverse (f []) $ tycPropTy d
    return d{tycDCons, tycPVars, tycSFun, tycPropTy}

emapDataCtorTyM
  :: Monad m
  => ([Symbol] -> ty -> m ty')
  -> DataCtorP ty
  -> m (DataCtorP ty')
emapDataCtorTyM :: forall (m :: * -> *) ty ty'.
Monad m =>
([Symbol] -> ty -> m ty') -> DataCtorP ty -> m (DataCtorP ty')
emapDataCtorTyM [Symbol] -> ty -> m ty'
f DataCtorP ty
d = do
    dcTheta <- (ty -> m ty') -> [ty] -> m [ty']
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ([Symbol] -> ty -> m ty'
f []) (DataCtorP ty -> [ty]
forall ty. DataCtorP ty -> [ty]
dcTheta DataCtorP ty
d)
    dcResult <- traverse (f (map (lhNameToUnqualifiedSymbol . fst) (dcFields d))) $ dcResult d
    dcFields <- snd <$> mapAccumM (\[Symbol]
γ  (LHName
s, ty
t) -> (HasCallStack => LHName -> Symbol
LHName -> Symbol
lhNameToUnqualifiedSymbol LHName
sSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
γ,) ((LHName, ty') -> ([Symbol], (LHName, ty')))
-> (ty' -> (LHName, ty')) -> ty' -> ([Symbol], (LHName, ty'))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LHName
s,) (ty' -> ([Symbol], (LHName, ty')))
-> m ty' -> m ([Symbol], (LHName, ty'))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> ty -> m ty'
f [Symbol]
γ ty
t) [] (dcFields d)
    return d{dcTheta, dcFields, dcResult}

emapExprArg :: ([b] -> ExprBV b v -> ExprBV b v) -> [b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
emapExprArg :: forall b v c tv r.
([b] -> ExprBV b v -> ExprBV b v)
-> [b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
emapExprArg [b] -> ExprBV b v -> ExprBV b v
f = [b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
go
  where
    go :: [b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
go [b]
_ t :: RTypeBV b v c tv r
t@RVar{}          = RTypeBV b v c tv r
t
    go [b]
_ t :: RTypeBV b v c tv r
t@RHole{}         = RTypeBV b v c tv r
t
    go [b]
γ (RAllT RTVUBV b v c tv
α RTypeBV b v c tv r
t r
r)     = RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
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 RTVUBV b v c tv
α ([b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
go [b]
γ RTypeBV b v c tv r
t) r
r
    go [b]
γ (RAllP PVUBV b v c tv
π RTypeBV b v c tv r
t)       = PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP PVUBV b v c tv
π ([b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
go [b]
γ RTypeBV b v c tv r
t)
    go [b]
γ (RFun b
x RFInfo
i RTypeBV b v c tv r
t RTypeBV b v c tv r
t' r
r) = b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
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  b
x RFInfo
i ([b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
go [b]
γ RTypeBV b v c tv r
t) ([b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
go (b
xb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
γ) RTypeBV b v c tv r
t') r
r
    go [b]
γ (RApp c
c [RTypeBV b v c tv r]
ts [RTPropBV b v c tv r]
rs r
r)  = c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
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  c
c ([b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
go [b]
γ (RTypeBV b v c tv r -> RTypeBV b v c tv r)
-> [RTypeBV b v c tv r] -> [RTypeBV b v c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeBV b v c tv r]
ts) ([b] -> RTPropBV b v c tv r -> RTPropBV b v c tv r
mo [b]
γ (RTPropBV b v c tv r -> RTPropBV b v c tv r)
-> [RTPropBV b v c tv r] -> [RTPropBV b v c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropBV b v c tv r]
rs) r
r
    go [b]
γ (RAllE b
z RTypeBV b v c tv r
t RTypeBV b v c tv r
t')    = b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
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 b
z ([b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
go [b]
γ RTypeBV b v c tv r
t) ([b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
go [b]
γ RTypeBV b v c tv r
t')
    go [b]
γ (REx b
z RTypeBV b v c tv r
t RTypeBV b v c tv r
t')      = b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
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   b
z ([b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
go [b]
γ RTypeBV b v c tv r
t) ([b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
go [b]
γ RTypeBV b v c tv r
t')
    go [b]
γ (RExprArg Located (ExprBV b v)
e)      = Located (ExprBV b v) -> RTypeBV b v c tv r
forall b v c tv r. Located (ExprBV b v) -> RTypeBV b v c tv r
RExprArg ([b] -> ExprBV b v -> ExprBV b v
f [b]
γ (ExprBV b v -> ExprBV b v)
-> Located (ExprBV b v) -> Located (ExprBV b v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located (ExprBV b v)
e) -- <---- actual substitution
    go [b]
γ (RAppTy RTypeBV b v c tv r
t RTypeBV b v c tv r
t' r
r)   = RTypeBV b v c tv r -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
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 ([b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
go [b]
γ RTypeBV b v c tv r
t) ([b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
go [b]
γ RTypeBV b v c tv r
t') r
r
    go [b]
γ (RRTy [(b, RTypeBV b v c tv r)]
e r
r Oblig
o RTypeBV b v c tv r
t)    = [(b, RTypeBV b v c tv r)]
-> r -> Oblig -> RTypeBV b v c tv r -> RTypeBV b v c tv r
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  ((RTypeBV b v c tv r -> RTypeBV b v c tv r)
-> (b, RTypeBV b v c tv r) -> (b, RTypeBV b v c tv r)
forall a b. (a -> b) -> (b, a) -> (b, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
go [b]
γ) ((b, RTypeBV b v c tv r) -> (b, RTypeBV b v c tv r))
-> [(b, RTypeBV b v c tv r)] -> [(b, RTypeBV b v c tv r)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(b, RTypeBV b v c tv r)]
e) r
r Oblig
o ([b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
go [b]
γ RTypeBV b v c tv r
t)

    mo :: [b] -> RTPropBV b v c tv r -> RTPropBV b v c tv r
mo [b]
_ t :: RTPropBV b v c tv r
t@(RProp [(b, RTypeBV b v c tv (NoReftB b))]
_ RHole{}) = RTPropBV b v c tv r
t
    mo [b]
γ (RProp [(b, RTypeBV b v c tv (NoReftB b))]
s RTypeBV b v c tv r
t)         = [(b, RTypeBV b v c tv (NoReftB b))]
-> RTypeBV b v c tv r -> RTPropBV b v c tv r
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(b, RTypeBV b v c tv (NoReftB b))]
s ([b] -> RTypeBV b v c tv r -> RTypeBV b v c tv r
go [b]
γ RTypeBV b v c tv r
t)

parsedToBareType :: BareTypeParsed -> BareType
parsedToBareType :: BareTypeParsed -> BareType
parsedToBareType = (Located Symbol -> Symbol)
-> RTypeBV Symbol (Located Symbol) BTyCon BTyVar RReft -> BareType
forall v v' b c tv r.
(v -> v') -> RTypeBV b v c tv r -> RTypeBV b v' c tv r
mapRTypeV Located Symbol -> Symbol
forall a. Located a -> a
F.val (RTypeBV Symbol (Located Symbol) BTyCon BTyVar RReft -> BareType)
-> (BareTypeParsed
    -> RTypeBV Symbol (Located Symbol) BTyCon BTyVar RReft)
-> BareTypeParsed
-> BareType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RReftV (Located Symbol) -> RReft)
-> BareTypeParsed
-> RTypeBV Symbol (Located Symbol) BTyCon BTyVar RReft
forall r1 r2 b v c tv.
(r1 -> r2) -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
mapReft ((Located Symbol -> Symbol)
-> (ReftBV Symbol (Located Symbol) -> ReftBV Symbol Symbol)
-> RReftV (Located Symbol)
-> RReft
forall v v' r r'.
(v -> v') -> (r -> r') -> UReftV v r -> UReftV v' r'
mapUReftV Located Symbol -> Symbol
forall a. Located a -> a
F.val ((Located Symbol -> Symbol)
-> ReftBV Symbol (Located Symbol) -> ReftBV Symbol Symbol
forall a b. (a -> b) -> ReftBV Symbol a -> ReftBV Symbol b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Located Symbol -> Symbol
forall a. Located a -> a
F.val))

foldRType :: (acc -> RType c tv r -> acc) -> acc -> RType c tv r -> acc
foldRType :: forall acc c tv r.
(acc -> RType c tv r -> acc) -> acc -> RType c tv r -> acc
foldRType acc -> RType c tv r -> acc
f = acc -> RType c tv r -> acc
go
  where
    step :: acc -> RType c tv r -> acc
step acc
a RType c tv r
t                = acc -> RType c tv r -> acc
go (acc -> RType c tv r -> acc
f acc
a RType c tv r
t) RType c tv r
t
    prep :: acc -> RTPropBV Symbol Symbol c tv r -> acc
prep acc
a (RProp [(Symbol, RTypeBV Symbol Symbol c tv (NoReftB Symbol))]
_ RHole{}) = acc
a
    prep acc
a (RProp [(Symbol, RTypeBV Symbol Symbol c tv (NoReftB Symbol))]
_ RType c tv r
t)      = acc -> RType c tv r -> acc
step acc
a RType c tv r
t
    go :: acc -> RType c tv r -> acc
go acc
a RVar{}             = acc
a
    go acc
a RHole{}            = acc
a
    go acc
a RExprArg{}         = acc
a
    go acc
a (RAllT RTVUBV Symbol Symbol c tv
_ RType c tv r
t r
_)      = acc -> RType c tv r -> acc
step acc
a RType c tv r
t
    go acc
a (RAllP PVUBV Symbol Symbol c tv
_ RType c tv r
t)        = acc -> RType c tv r -> acc
step acc
a RType c tv r
t
    go acc
a (RFun Symbol
_ RFInfo
_ RType c tv r
t RType c tv r
t' r
_)  = (acc -> RType c tv r -> acc) -> acc -> [RType c tv r] -> acc
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' acc -> RType c tv r -> acc
step acc
a [RType c tv r
t, RType c tv r
t']
    go acc
a (RAllE Symbol
_ RType c tv r
t RType c tv r
t')     = (acc -> RType c tv r -> acc) -> acc -> [RType c tv r] -> acc
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' acc -> RType c tv r -> acc
step acc
a [RType c tv r
t, RType c tv r
t']
    go acc
a (REx Symbol
_ RType c tv r
t RType c tv r
t')       = (acc -> RType c tv r -> acc) -> acc -> [RType c tv r] -> acc
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' acc -> RType c tv r -> acc
step acc
a [RType c tv r
t, RType c tv r
t']
    go acc
a (RAppTy RType c tv r
t RType c tv r
t' r
_)    = (acc -> RType c tv r -> acc) -> acc -> [RType c tv r] -> acc
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' acc -> RType c tv r -> acc
step acc
a [RType c tv r
t, RType c tv r
t']
    go acc
a (RApp c
_ [RType c tv r]
ts [RTPropBV Symbol Symbol c tv r]
rs r
_)   = (acc -> RTPropBV Symbol Symbol c tv r -> acc)
-> acc -> [RTPropBV Symbol Symbol c tv r] -> acc
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' acc -> RTPropBV Symbol Symbol c tv r -> acc
prep ((acc -> RType c tv r -> acc) -> acc -> [RType c tv r] -> acc
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' acc -> RType c tv r -> acc
step acc
a [RType c tv r]
ts) [RTPropBV Symbol Symbol c tv r]
rs
    go acc
a (RRTy [(Symbol, RType c tv r)]
e r
_ Oblig
_ RType c tv r
t)     = (acc -> RType c tv r -> acc) -> acc -> [RType c tv r] -> acc
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' acc -> RType c tv r -> acc
step acc
a (RType c tv r
t RType c tv r -> [RType c tv r] -> [RType c tv r]
forall a. a -> [a] -> [a]
: ((Symbol, RType c tv r) -> RType c tv r
forall a b. (a, b) -> b
snd ((Symbol, RType c tv r) -> RType c tv r)
-> [(Symbol, RType c tv r)] -> [RType c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv r)]
e))

------------------------------------------------------------------------------------------------------
-- isBase' x t = traceShow ("isBase: " ++ showpp x) $ isBase t
-- same as GhcMisc isBaseType

-- isBase :: RType a -> Bool

-- set all types to basic types, haskell `tx -> t` is translated to Arrow tx t
-- isBase _ = True

isBase :: RType t t1 t2 -> Bool
isBase :: forall t t1 t2. RType t t1 t2 -> Bool
isBase (RAllT RTVUBV Symbol Symbol t t1
_ RTypeBV Symbol Symbol t t1 t2
t t2
_)    = RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase RTypeBV Symbol Symbol t t1 t2
t
isBase (RAllP PVUBV Symbol Symbol t t1
_ RTypeBV Symbol Symbol t t1 t2
t)      = RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase RTypeBV Symbol Symbol t t1 t2
t
isBase (RVar t1
_ t2
_)       = Bool
True
isBase (RApp t
_ [RTypeBV Symbol Symbol t t1 t2]
ts [RTPropBV Symbol Symbol t t1 t2]
_ t2
_)  = (RTypeBV Symbol Symbol t t1 t2 -> Bool)
-> [RTypeBV Symbol Symbol t t1 t2] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase [RTypeBV Symbol Symbol t t1 t2]
ts
isBase RFun{}           = Bool
False
isBase (RAppTy RTypeBV Symbol Symbol t t1 t2
t1 RTypeBV Symbol Symbol t t1 t2
t2 t2
_) = RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase RTypeBV Symbol Symbol t t1 t2
t1 Bool -> Bool -> Bool
&& RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase RTypeBV Symbol Symbol t t1 t2
t2
isBase (RRTy [(Symbol, RTypeBV Symbol Symbol t t1 t2)]
_ t2
_ Oblig
_ RTypeBV Symbol Symbol t t1 t2
t)   = RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase RTypeBV Symbol Symbol t t1 t2
t
isBase (RAllE Symbol
_ RTypeBV Symbol Symbol t t1 t2
_ RTypeBV Symbol Symbol t t1 t2
t)    = RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase RTypeBV Symbol Symbol t t1 t2
t
isBase (REx Symbol
_ RTypeBV Symbol Symbol t t1 t2
_ RTypeBV Symbol Symbol t t1 t2
t)      = RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase RTypeBV Symbol Symbol t t1 t2
t
isBase RTypeBV Symbol Symbol t t1 t2
_                = Bool
False

hasHoleTy :: RType t t1 t2 -> Bool
hasHoleTy :: forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy (RVar t1
_ t2
_)        = Bool
False
hasHoleTy (RAllT RTVUBV Symbol Symbol t t1
_ RTypeBV Symbol Symbol t t1 t2
t t2
_)     = RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeBV Symbol Symbol t t1 t2
t
hasHoleTy (RAllP PVUBV Symbol Symbol t t1
_ RTypeBV Symbol Symbol t t1 t2
t)       = RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeBV Symbol Symbol t t1 t2
t
hasHoleTy (RFun Symbol
_ RFInfo
_ RTypeBV Symbol Symbol t t1 t2
t RTypeBV Symbol Symbol t t1 t2
t' t2
_) = RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeBV Symbol Symbol t t1 t2
t Bool -> Bool -> Bool
|| RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeBV Symbol Symbol t t1 t2
t'
hasHoleTy (RApp t
_ [RTypeBV Symbol Symbol t t1 t2]
ts [RTPropBV Symbol Symbol t t1 t2]
_ t2
_)   = (RTypeBV Symbol Symbol t t1 t2 -> Bool)
-> [RTypeBV Symbol Symbol t t1 t2] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy [RTypeBV Symbol Symbol t t1 t2]
ts
hasHoleTy (RAllE Symbol
_ RTypeBV Symbol Symbol t t1 t2
t RTypeBV Symbol Symbol t t1 t2
t')    = RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeBV Symbol Symbol t t1 t2
t Bool -> Bool -> Bool
|| RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeBV Symbol Symbol t t1 t2
t'
hasHoleTy (REx Symbol
_ RTypeBV Symbol Symbol t t1 t2
t RTypeBV Symbol Symbol t t1 t2
t')      = RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeBV Symbol Symbol t t1 t2
t Bool -> Bool -> Bool
|| RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeBV Symbol Symbol t t1 t2
t'
hasHoleTy (RExprArg Located (ExprBV Symbol Symbol)
_)      = Bool
False
hasHoleTy (RAppTy RTypeBV Symbol Symbol t t1 t2
t RTypeBV Symbol Symbol t t1 t2
t' t2
_)   = RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeBV Symbol Symbol t t1 t2
t Bool -> Bool -> Bool
|| RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeBV Symbol Symbol t t1 t2
t'
hasHoleTy (RHole t2
_)         = Bool
True
hasHoleTy (RRTy [(Symbol, RTypeBV Symbol Symbol t t1 t2)]
xts t2
_ Oblig
_ RTypeBV Symbol Symbol t t1 t2
t)  = RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeBV Symbol Symbol t t1 t2
t Bool -> Bool -> Bool
|| (RTypeBV Symbol Symbol t t1 t2 -> Bool)
-> [RTypeBV Symbol Symbol t t1 t2] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy ((Symbol, RTypeBV Symbol Symbol t t1 t2)
-> RTypeBV Symbol Symbol t t1 t2
forall a b. (a, b) -> b
snd ((Symbol, RTypeBV Symbol Symbol t t1 t2)
 -> RTypeBV Symbol Symbol t t1 t2)
-> [(Symbol, RTypeBV Symbol Symbol t t1 t2)]
-> [RTypeBV Symbol Symbol t t1 t2]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RTypeBV Symbol Symbol t t1 t2)]
xts)

isFunTy :: RType t t1 t2 -> Bool
isFunTy :: forall t t1 t2. RType t t1 t2 -> Bool
isFunTy (RAllE Symbol
_ RTypeBV Symbol Symbol t t1 t2
_ RTypeBV Symbol Symbol t t1 t2
t)    = RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isFunTy RTypeBV Symbol Symbol t t1 t2
t
isFunTy (RAllT RTVUBV Symbol Symbol t t1
_ RTypeBV Symbol Symbol t t1 t2
t t2
_)    = RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isFunTy RTypeBV Symbol Symbol t t1 t2
t
isFunTy (RAllP PVUBV Symbol Symbol t t1
_ RTypeBV Symbol Symbol t t1 t2
t)      = RTypeBV Symbol Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isFunTy RTypeBV Symbol Symbol t t1 t2
t
isFunTy RFun{}           = Bool
True
isFunTy RTypeBV Symbol Symbol t t1 t2
_                = Bool
False

mapReftM :: (Monad m) => (r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapReftM :: forall (m :: * -> *) r1 r2 c tv.
Monad m =>
(r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapReftM r1 -> m r2
f (RVar tv
α r1
r)        = (r2 -> RType c tv r2) -> m r2 -> m (RType c tv r2)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap   (tv -> r2 -> RType c tv r2
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar  tv
α)  (r1 -> m r2
f r1
r)
mapReftM r1 -> m r2
f (RAllT RTVUBV Symbol Symbol c tv
α RTypeBV Symbol Symbol c tv r1
t r1
r)     = (RType c tv r2 -> r2 -> RType c tv r2)
-> m (RType c tv r2) -> m r2 -> m (RType c tv r2)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (RTVUBV Symbol Symbol c tv -> RType c tv r2 -> r2 -> RType c tv r2
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 RTVUBV Symbol Symbol c tv
α)  ((r1 -> m r2) -> RTypeBV Symbol Symbol c tv r1 -> m (RType c tv r2)
forall (m :: * -> *) r1 r2 c tv.
Monad m =>
(r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapReftM r1 -> m r2
f RTypeBV Symbol Symbol c tv r1
t)         (r1 -> m r2
f r1
r)
mapReftM r1 -> m r2
f (RAllP PVUBV Symbol Symbol c tv
π RTypeBV Symbol Symbol c tv r1
t)       = (RType c tv r2 -> RType c tv r2)
-> m (RType c tv r2) -> m (RType c tv r2)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap   (PVUBV Symbol Symbol c tv -> RType c tv r2 -> RType c tv r2
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP PVUBV Symbol Symbol c tv
π)  ((r1 -> m r2) -> RTypeBV Symbol Symbol c tv r1 -> m (RType c tv r2)
forall (m :: * -> *) r1 r2 c tv.
Monad m =>
(r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapReftM r1 -> m r2
f RTypeBV Symbol Symbol c tv r1
t)
mapReftM r1 -> m r2
f (RFun Symbol
x RFInfo
i RTypeBV Symbol Symbol c tv r1
t RTypeBV Symbol Symbol c tv r1
t' r1
r) = (RType c tv r2 -> RType c tv r2 -> r2 -> RType c tv r2)
-> m (RType c tv r2)
-> m (RType c tv r2)
-> m r2
-> m (RType c tv r2)
forall (m :: * -> *) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3 (Symbol
-> RFInfo -> RType c tv r2 -> RType c tv r2 -> r2 -> RType c tv r2
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
x RFInfo
i) ((r1 -> m r2) -> RTypeBV Symbol Symbol c tv r1 -> m (RType c tv r2)
forall (m :: * -> *) r1 r2 c tv.
Monad m =>
(r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapReftM r1 -> m r2
f RTypeBV Symbol Symbol c tv r1
t)         ((r1 -> m r2) -> RTypeBV Symbol Symbol c tv r1 -> m (RType c tv r2)
forall (m :: * -> *) r1 r2 c tv.
Monad m =>
(r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapReftM r1 -> m r2
f RTypeBV Symbol Symbol c tv r1
t')       (r1 -> m r2
f r1
r)
mapReftM r1 -> m r2
f (RApp c
c [RTypeBV Symbol Symbol c tv r1]
ts [RTPropBV Symbol Symbol c tv r1]
rs r1
r)  = ([RType c tv r2]
 -> [RTPropBV Symbol Symbol c tv r2] -> r2 -> RType c tv r2)
-> m [RType c tv r2]
-> m [RTPropBV Symbol Symbol c tv r2]
-> m r2
-> m (RType c tv r2)
forall (m :: * -> *) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3 (c
-> [RType c tv r2]
-> [RTPropBV Symbol Symbol c tv r2]
-> r2
-> RType c tv r2
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  c
c)  ((RTypeBV Symbol Symbol c tv r1 -> m (RType c tv r2))
-> [RTypeBV Symbol Symbol c tv r1] -> m [RType c tv r2]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((r1 -> m r2) -> RTypeBV Symbol Symbol c tv r1 -> m (RType c tv r2)
forall (m :: * -> *) r1 r2 c tv.
Monad m =>
(r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapReftM r1 -> m r2
f) [RTypeBV Symbol Symbol c tv r1]
ts) ((RTPropBV Symbol Symbol c tv r1
 -> m (RTPropBV Symbol Symbol c tv r2))
-> [RTPropBV Symbol Symbol c tv r1]
-> m [RTPropBV Symbol Symbol c tv r2]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((r1 -> m r2)
-> RTPropBV Symbol Symbol c tv r1
-> m (RTPropBV Symbol Symbol c tv r2)
forall (m :: * -> *) t s c tv.
Monad m =>
(t -> m s) -> RTProp c tv t -> m (RTProp c tv s)
mapRefM r1 -> m r2
f) [RTPropBV Symbol Symbol c tv r1]
rs) (r1 -> m r2
f r1
r)
mapReftM r1 -> m r2
f (RAllE Symbol
z RTypeBV Symbol Symbol c tv r1
t RTypeBV Symbol Symbol c tv r1
t')    = (RType c tv r2 -> RType c tv r2 -> RType c tv r2)
-> m (RType c tv r2) -> m (RType c tv r2) -> m (RType c tv r2)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Symbol -> RType c tv r2 -> RType c tv r2 -> RType c tv r2
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
z)  ((r1 -> m r2) -> RTypeBV Symbol Symbol c tv r1 -> m (RType c tv r2)
forall (m :: * -> *) r1 r2 c tv.
Monad m =>
(r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapReftM r1 -> m r2
f RTypeBV Symbol Symbol c tv r1
t)         ((r1 -> m r2) -> RTypeBV Symbol Symbol c tv r1 -> m (RType c tv r2)
forall (m :: * -> *) r1 r2 c tv.
Monad m =>
(r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapReftM r1 -> m r2
f RTypeBV Symbol Symbol c tv r1
t')
mapReftM r1 -> m r2
f (REx Symbol
z RTypeBV Symbol Symbol c tv r1
t RTypeBV Symbol Symbol c tv r1
t')      = (RType c tv r2 -> RType c tv r2 -> RType c tv r2)
-> m (RType c tv r2) -> m (RType c tv r2) -> m (RType c tv r2)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Symbol -> RType c tv r2 -> RType c tv r2 -> RType c tv r2
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
z)    ((r1 -> m r2) -> RTypeBV Symbol Symbol c tv r1 -> m (RType c tv r2)
forall (m :: * -> *) r1 r2 c tv.
Monad m =>
(r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapReftM r1 -> m r2
f RTypeBV Symbol Symbol c tv r1
t)         ((r1 -> m r2) -> RTypeBV Symbol Symbol c tv r1 -> m (RType c tv r2)
forall (m :: * -> *) r1 r2 c tv.
Monad m =>
(r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapReftM r1 -> m r2
f RTypeBV Symbol Symbol c tv r1
t')
mapReftM r1 -> m r2
_ (RExprArg Located (ExprBV Symbol Symbol)
e)      = RType c tv r2 -> m (RType c tv r2)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (RType c tv r2 -> m (RType c tv r2))
-> RType c tv r2 -> m (RType c tv r2)
forall a b. (a -> b) -> a -> b
$ Located (ExprBV Symbol Symbol) -> RType c tv r2
forall b v c tv r. Located (ExprBV b v) -> RTypeBV b v c tv r
RExprArg Located (ExprBV Symbol Symbol)
e
mapReftM r1 -> m r2
f (RAppTy RTypeBV Symbol Symbol c tv r1
t RTypeBV Symbol Symbol c tv r1
t' r1
r)   = (RType c tv r2 -> RType c tv r2 -> r2 -> RType c tv r2)
-> m (RType c tv r2)
-> m (RType c tv r2)
-> m r2
-> m (RType c tv r2)
forall (m :: * -> *) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3 RType c tv r2 -> RType c tv r2 -> r2 -> RType c tv r2
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 ((r1 -> m r2) -> RTypeBV Symbol Symbol c tv r1 -> m (RType c tv r2)
forall (m :: * -> *) r1 r2 c tv.
Monad m =>
(r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapReftM r1 -> m r2
f RTypeBV Symbol Symbol c tv r1
t) ((r1 -> m r2) -> RTypeBV Symbol Symbol c tv r1 -> m (RType c tv r2)
forall (m :: * -> *) r1 r2 c tv.
Monad m =>
(r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapReftM r1 -> m r2
f RTypeBV Symbol Symbol c tv r1
t') (r1 -> m r2
f r1
r)
mapReftM r1 -> m r2
f (RHole r1
r)         = (r2 -> RType c tv r2) -> m r2 -> m (RType c tv r2)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap   r2 -> RType c tv r2
forall b v c tv r. r -> RTypeBV b v c tv r
RHole      (r1 -> m r2
f r1
r)
mapReftM r1 -> m r2
f (RRTy [(Symbol, RTypeBV Symbol Symbol c tv r1)]
xts r1
r Oblig
o RTypeBV Symbol Symbol c tv r1
t)  = ([(Symbol, RType c tv r2)]
 -> r2 -> Oblig -> RType c tv r2 -> RType c tv r2)
-> m [(Symbol, RType c tv r2)]
-> m r2
-> m Oblig
-> m (RType c tv r2)
-> m (RType c tv r2)
forall (m :: * -> *) a1 a2 a3 a4 r.
Monad m =>
(a1 -> a2 -> a3 -> a4 -> r) -> m a1 -> m a2 -> m a3 -> m a4 -> m r
liftM4 [(Symbol, RType c tv r2)]
-> r2 -> Oblig -> RType c tv r2 -> RType c tv r2
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 c tv r1)
 -> m (Symbol, RType c tv r2))
-> [(Symbol, RTypeBV Symbol Symbol c tv r1)]
-> m [(Symbol, RType c tv r2)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((RTypeBV Symbol Symbol c tv r1 -> m (RType c tv r2))
-> (Symbol, RTypeBV Symbol Symbol c tv r1)
-> m (Symbol, RType c tv r2)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (Symbol, a) -> f (Symbol, b)
traverse ((r1 -> m r2) -> RTypeBV Symbol Symbol c tv r1 -> m (RType c tv r2)
forall (m :: * -> *) r1 r2 c tv.
Monad m =>
(r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapReftM r1 -> m r2
f)) [(Symbol, RTypeBV Symbol Symbol c tv r1)]
xts) (r1 -> m r2
f r1
r) (Oblig -> m Oblig
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Oblig
o) ((r1 -> m r2) -> RTypeBV Symbol Symbol c tv r1 -> m (RType c tv r2)
forall (m :: * -> *) r1 r2 c tv.
Monad m =>
(r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapReftM r1 -> m r2
f RTypeBV Symbol Symbol c tv r1
t)

mapRefM  :: (Monad m) => (t -> m s) -> RTProp c tv t -> m (RTProp c tv s)
mapRefM :: forall (m :: * -> *) t s c tv.
Monad m =>
(t -> m s) -> RTProp c tv t -> m (RTProp c tv s)
mapRefM  t -> m s
f (RProp [(Symbol, RTypeBV Symbol Symbol c tv (NoReftB Symbol))]
s RTypeBV Symbol Symbol c tv t
t)        = (RTypeBV Symbol Symbol c tv s -> RTProp c tv s)
-> m (RTypeBV Symbol Symbol c tv s) -> m (RTProp c tv s)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap    ([(Symbol, RTypeBV Symbol Symbol c tv (NoReftB Symbol))]
-> RTypeBV Symbol Symbol c tv s -> RTProp c tv s
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(Symbol, RTypeBV Symbol Symbol c tv (NoReftB Symbol))]
s)      ((t -> m s)
-> RTypeBV Symbol Symbol c tv t -> m (RTypeBV Symbol Symbol c tv s)
forall (m :: * -> *) r1 r2 c tv.
Monad m =>
(r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
mapReftM t -> m s
f RTypeBV Symbol Symbol c tv t
t)

mapPropM :: (Monad m) => (RTProp c tv r -> m (RTProp c tv r)) -> RType c tv r -> m (RType c tv r)
mapPropM :: forall (m :: * -> *) c tv r.
Monad m =>
(RTProp c tv r -> m (RTProp c tv r))
-> RType c tv r -> m (RType c tv r)
mapPropM RTProp c tv r -> m (RTProp c tv r)
_ (RVar tv
α r
r)        = RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r))
-> RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r)
forall a b. (a -> b) -> a -> b
$ tv -> r -> RTypeBV Symbol Symbol c tv r
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar  tv
α r
r
mapPropM RTProp c tv r -> m (RTProp c tv r)
f (RAllT RTVUBV Symbol Symbol c tv
α RTypeBV Symbol Symbol c tv r
t r
r)     = (RTypeBV Symbol Symbol c tv r -> r -> RTypeBV Symbol Symbol c tv r)
-> m (RTypeBV Symbol Symbol c tv r)
-> m r
-> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (RTVUBV Symbol Symbol c tv
-> RTypeBV Symbol Symbol c tv r
-> r
-> RTypeBV Symbol Symbol c tv r
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 RTVUBV Symbol Symbol c tv
α)   ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) c tv r.
Monad m =>
(RTProp c tv r -> m (RTProp c tv r))
-> RType c tv r -> m (RType c tv r)
mapPropM RTProp c tv r -> m (RTProp c tv r)
f RTypeBV Symbol Symbol c tv r
t)          (r -> m r
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return r
r)
mapPropM RTProp c tv r -> m (RTProp c tv r)
f (RAllP PVUBV Symbol Symbol c tv
π RTypeBV Symbol Symbol c tv r
t)       = (RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r)
-> m (RTypeBV Symbol Symbol c tv r)
-> m (RTypeBV Symbol Symbol c tv r)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap   (PVUBV Symbol Symbol c tv
-> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP PVUBV Symbol Symbol c tv
π)   ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) c tv r.
Monad m =>
(RTProp c tv r -> m (RTProp c tv r))
-> RType c tv r -> m (RType c tv r)
mapPropM RTProp c tv r -> m (RTProp c tv r)
f RTypeBV Symbol Symbol c tv r
t)
mapPropM RTProp c tv r -> m (RTProp c tv r)
f (RFun Symbol
x RFInfo
i RTypeBV Symbol Symbol c tv r
t RTypeBV Symbol Symbol c tv r
t' r
r) = (RTypeBV Symbol Symbol c tv r
 -> RTypeBV Symbol Symbol c tv r
 -> r
 -> RTypeBV Symbol Symbol c tv r)
-> m (RTypeBV Symbol Symbol c tv r)
-> m (RTypeBV Symbol Symbol c tv r)
-> m r
-> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3 (Symbol
-> RFInfo
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
-> r
-> RTypeBV Symbol Symbol c tv r
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
x RFInfo
i)  ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) c tv r.
Monad m =>
(RTProp c tv r -> m (RTProp c tv r))
-> RType c tv r -> m (RType c tv r)
mapPropM RTProp c tv r -> m (RTProp c tv r)
f RTypeBV Symbol Symbol c tv r
t)          ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) c tv r.
Monad m =>
(RTProp c tv r -> m (RTProp c tv r))
-> RType c tv r -> m (RType c tv r)
mapPropM RTProp c tv r -> m (RTProp c tv r)
f RTypeBV Symbol Symbol c tv r
t') (r -> m r
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return r
r)
mapPropM RTProp c tv r -> m (RTProp c tv r)
f (RApp c
c [RTypeBV Symbol Symbol c tv r]
ts [RTProp c tv r]
rs r
r)  = ([RTypeBV Symbol Symbol c tv r]
 -> [RTProp c tv r] -> r -> RTypeBV Symbol Symbol c tv r)
-> m [RTypeBV Symbol Symbol c tv r]
-> m [RTProp c tv r]
-> m r
-> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3 (c
-> [RTypeBV Symbol Symbol c tv r]
-> [RTProp c tv r]
-> r
-> RTypeBV Symbol Symbol c tv r
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  c
c)   ((RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r))
-> [RTypeBV Symbol Symbol c tv r]
-> m [RTypeBV Symbol Symbol c tv r]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) c tv r.
Monad m =>
(RTProp c tv r -> m (RTProp c tv r))
-> RType c tv r -> m (RType c tv r)
mapPropM RTProp c tv r -> m (RTProp c tv r)
f) [RTypeBV Symbol Symbol c tv r]
ts)  ((RTProp c tv r -> m (RTProp c tv r))
-> [RTProp c tv r] -> m [RTProp c tv r]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM RTProp c tv r -> m (RTProp c tv r)
f [RTProp c tv r]
rs)     (r -> m r
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return r
r)
mapPropM RTProp c tv r -> m (RTProp c tv r)
f (RAllE Symbol
z RTypeBV Symbol Symbol c tv r
t RTypeBV Symbol Symbol c tv r
t')    = (RTypeBV Symbol Symbol c tv r
 -> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r)
-> m (RTypeBV Symbol Symbol c tv r)
-> m (RTypeBV Symbol Symbol c tv r)
-> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Symbol
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
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
z)   ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) c tv r.
Monad m =>
(RTProp c tv r -> m (RTProp c tv r))
-> RType c tv r -> m (RType c tv r)
mapPropM RTProp c tv r -> m (RTProp c tv r)
f RTypeBV Symbol Symbol c tv r
t)          ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) c tv r.
Monad m =>
(RTProp c tv r -> m (RTProp c tv r))
-> RType c tv r -> m (RType c tv r)
mapPropM RTProp c tv r -> m (RTProp c tv r)
f RTypeBV Symbol Symbol c tv r
t')
mapPropM RTProp c tv r -> m (RTProp c tv r)
f (REx Symbol
z RTypeBV Symbol Symbol c tv r
t RTypeBV Symbol Symbol c tv r
t')      = (RTypeBV Symbol Symbol c tv r
 -> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r)
-> m (RTypeBV Symbol Symbol c tv r)
-> m (RTypeBV Symbol Symbol c tv r)
-> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Symbol
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
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
z)     ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) c tv r.
Monad m =>
(RTProp c tv r -> m (RTProp c tv r))
-> RType c tv r -> m (RType c tv r)
mapPropM RTProp c tv r -> m (RTProp c tv r)
f RTypeBV Symbol Symbol c tv r
t)          ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) c tv r.
Monad m =>
(RTProp c tv r -> m (RTProp c tv r))
-> RType c tv r -> m (RType c tv r)
mapPropM RTProp c tv r -> m (RTProp c tv r)
f RTypeBV Symbol Symbol c tv r
t')
mapPropM RTProp c tv r -> m (RTProp c tv r)
_ (RExprArg Located (ExprBV Symbol Symbol)
e)      = RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r))
-> RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r)
forall a b. (a -> b) -> a -> b
$ Located (ExprBV Symbol Symbol) -> RTypeBV Symbol Symbol c tv r
forall b v c tv r. Located (ExprBV b v) -> RTypeBV b v c tv r
RExprArg Located (ExprBV Symbol Symbol)
e
mapPropM RTProp c tv r -> m (RTProp c tv r)
f (RAppTy RTypeBV Symbol Symbol c tv r
t RTypeBV Symbol Symbol c tv r
t' r
r)   = (RTypeBV Symbol Symbol c tv r
 -> RTypeBV Symbol Symbol c tv r
 -> r
 -> RTypeBV Symbol Symbol c tv r)
-> m (RTypeBV Symbol Symbol c tv r)
-> m (RTypeBV Symbol Symbol c tv r)
-> m r
-> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3 RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
-> r
-> RTypeBV Symbol Symbol c tv r
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 ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) c tv r.
Monad m =>
(RTProp c tv r -> m (RTProp c tv r))
-> RType c tv r -> m (RType c tv r)
mapPropM RTProp c tv r -> m (RTProp c tv r)
f RTypeBV Symbol Symbol c tv r
t) ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) c tv r.
Monad m =>
(RTProp c tv r -> m (RTProp c tv r))
-> RType c tv r -> m (RType c tv r)
mapPropM RTProp c tv r -> m (RTProp c tv r)
f RTypeBV Symbol Symbol c tv r
t') (r -> m r
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return r
r)
mapPropM RTProp c tv r -> m (RTProp c tv r)
_ (RHole r
r)         = RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r))
-> RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r)
forall a b. (a -> b) -> a -> b
$ r -> RTypeBV Symbol Symbol c tv r
forall b v c tv r. r -> RTypeBV b v c tv r
RHole r
r
mapPropM RTProp c tv r -> m (RTProp c tv r)
f (RRTy [(Symbol, RTypeBV Symbol Symbol c tv r)]
xts r
r Oblig
o RTypeBV Symbol Symbol c tv r
t)  = ([(Symbol, RTypeBV Symbol Symbol c tv r)]
 -> r
 -> Oblig
 -> RTypeBV Symbol Symbol c tv r
 -> RTypeBV Symbol Symbol c tv r)
-> m [(Symbol, RTypeBV Symbol Symbol c tv r)]
-> m r
-> m Oblig
-> m (RTypeBV Symbol Symbol c tv r)
-> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) a1 a2 a3 a4 r.
Monad m =>
(a1 -> a2 -> a3 -> a4 -> r) -> m a1 -> m a2 -> m a3 -> m a4 -> m r
liftM4 [(Symbol, RTypeBV Symbol Symbol c tv r)]
-> r
-> Oblig
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
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 c tv r)
 -> m (Symbol, RTypeBV Symbol Symbol c tv r))
-> [(Symbol, RTypeBV Symbol Symbol c tv r)]
-> m [(Symbol, RTypeBV Symbol Symbol c tv r)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r))
-> (Symbol, RTypeBV Symbol Symbol c tv r)
-> m (Symbol, RTypeBV Symbol Symbol c tv r)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (Symbol, a) -> f (Symbol, b)
traverse ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) c tv r.
Monad m =>
(RTProp c tv r -> m (RTProp c tv r))
-> RType c tv r -> m (RType c tv r)
mapPropM RTProp c tv r -> m (RTProp c tv r)
f)) [(Symbol, RTypeBV Symbol Symbol c tv r)]
xts) (r -> m r
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return r
r) (Oblig -> m Oblig
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Oblig
o) ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeBV Symbol Symbol c tv r -> m (RTypeBV Symbol Symbol c tv r)
forall (m :: * -> *) c tv r.
Monad m =>
(RTProp c tv r -> m (RTProp c tv r))
-> RType c tv r -> m (RType c tv r)
mapPropM RTProp c tv r -> m (RTProp c tv r)
f RTypeBV Symbol Symbol c tv r
t)


--------------------------------------------------------------------------------
foldReft :: (IsReft r, TyConable c, F.Binder b, ReftBind r ~ b) => BScope -> (F.SEnvB b (RTypeBV b v c tv r) -> r -> z -> z) -> z -> RTypeBV b v c tv r -> z
--------------------------------------------------------------------------------
foldReft :: forall r c b v tv z.
(IsReft r, TyConable c, Binder b, ReftBind r ~ b) =>
Bool
-> (SEnvB b (RTypeBV b v c tv r) -> r -> z -> z)
-> z
-> RTypeBV b v c tv r
-> z
foldReft Bool
bsc SEnvB b (RTypeBV b v c tv r) -> r -> z -> z
f = Bool
-> (RTypeBV b v c tv r -> RTypeBV b v c tv r)
-> (SEnvB b (RTypeBV b v c tv r)
    -> Maybe (RTypeBV b v c tv r) -> r -> z -> z)
-> z
-> RTypeBV b v c tv r
-> z
forall r c b v tv a z.
(IsReft r, TyConable c, Binder b, ReftBind r ~ b) =>
Bool
-> (RTypeBV b v c tv r -> a)
-> (SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z)
-> z
-> RTypeBV b v c tv r
-> z
foldReft' Bool
bsc RTypeBV b v c tv r -> RTypeBV b v c tv r
forall a. a -> a
id (\SEnvB b (RTypeBV b v c tv r)
γ Maybe (RTypeBV b v c tv r)
_ -> SEnvB b (RTypeBV b v c tv r) -> r -> z -> z
f SEnvB b (RTypeBV b v c tv r)
γ)

--------------------------------------------------------------------------------
foldReft' :: (IsReft r, TyConable c, F.Binder b, ReftBind r ~ b)
          => BScope
          -> (RTypeBV b v c tv r -> a)
          -> (F.SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z)
          -> z -> RTypeBV b v c tv r -> z
--------------------------------------------------------------------------------
foldReft' :: forall r c b v tv a z.
(IsReft r, TyConable c, Binder b, ReftBind r ~ b) =>
Bool
-> (RTypeBV b v c tv r -> a)
-> (SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z)
-> z
-> RTypeBV b v c tv r
-> z
foldReft' Bool
bsc RTypeBV b v c tv r -> a
g SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z
f
  = Bool
-> (c -> [RTypeBV b v c tv r] -> [(b, a)])
-> (RTVar tv (RTypeBV b v c tv (NoReftB b)) -> [(b, a)])
-> (RTypeBV b v c tv r -> a)
-> (SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z)
-> (PVarBV b v (RTypeBV b v c tv (NoReftB b))
    -> SEnvB b a -> SEnvB b a)
-> SEnvB b a
-> z
-> RTypeBV b v c tv r
-> z
forall r c b v tv a z.
(IsReft r, TyConable c, Binder b, ReftBind r ~ b) =>
Bool
-> (c -> [RTypeBV b v c tv r] -> [(b, a)])
-> (RTVar tv (RTypeBV b v c tv (NoReftB b)) -> [(b, a)])
-> (RTypeBV b v c tv r -> a)
-> (SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z)
-> (PVarBV b v (RTypeBV b v c tv (NoReftB b))
    -> SEnvB b a -> SEnvB b a)
-> SEnvB b a
-> z
-> RTypeBV b v c tv r
-> z
efoldReft Bool
bsc
              (\c
_ [RTypeBV b v c tv r]
_ -> [])
              ([(b, a)] -> RTVar tv (RTypeBV b v c tv (NoReftB b)) -> [(b, a)]
forall a b. a -> b -> a
const [])
              RTypeBV b v c tv r -> a
g
              (\SEnvB b a
γ Maybe (RTypeBV b v c tv r)
t r
r z
z -> SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z
f SEnvB b a
γ Maybe (RTypeBV b v c tv r)
t r
r z
z)
              (\PVarBV b v (RTypeBV b v c tv (NoReftB b))
_ SEnvB b a
γ -> SEnvB b a
γ)
              SEnvB b a
forall b a. SEnvB b a
F.emptySEnv

tyVarIsVal :: RTVar tv s -> Bool
tyVarIsVal :: forall tv s. RTVar tv s -> Bool
tyVarIsVal = RTVInfo s -> Bool
forall s. RTVInfo s -> Bool
rtvinfoIsVal (RTVInfo s -> Bool)
-> (RTVar tv s -> RTVInfo s) -> RTVar tv s -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTVar tv s -> RTVInfo s
forall tv s. RTVar tv s -> RTVInfo s
ty_var_info

rtvinfoIsVal :: RTVInfo s -> Bool
rtvinfoIsVal :: forall s. RTVInfo s -> Bool
rtvinfoIsVal RTVNoInfo{} = Bool
False
rtvinfoIsVal RTVInfo{s
Bool
Symbol
rtv_name :: Symbol
rtv_kind :: s
rtv_is_val :: Bool
rtv_is_pol :: Bool
rtv_is_pol :: forall s. RTVInfo s -> Bool
rtv_is_val :: forall s. RTVInfo s -> Bool
rtv_kind :: forall s. RTVInfo s -> s
rtv_name :: forall s. RTVInfo s -> Symbol
..} = Bool
rtv_is_val

efoldReft :: (IsReft r, TyConable c, F.Binder b, ReftBind r ~ b)
          => BScope
          -> (c  -> [RTypeBV b v c tv r] -> [(b, a)])
          -> (RTVar tv (RTypeBV b v c tv (NoReftB b)) -> [(b, a)])
          -> (RTypeBV b v c tv r -> a)
          -> (F.SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z)
          -> (PVarBV b v (RTypeBV b v c tv (NoReftB b)) -> F.SEnvB b a -> F.SEnvB b a)
          -> F.SEnvB b a
          -> z
          -> RTypeBV b v c tv r
          -> z
efoldReft :: forall r c b v tv a z.
(IsReft r, TyConable c, Binder b, ReftBind r ~ b) =>
Bool
-> (c -> [RTypeBV b v c tv r] -> [(b, a)])
-> (RTVar tv (RTypeBV b v c tv (NoReftB b)) -> [(b, a)])
-> (RTypeBV b v c tv r -> a)
-> (SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z)
-> (PVarBV b v (RTypeBV b v c tv (NoReftB b))
    -> SEnvB b a -> SEnvB b a)
-> SEnvB b a
-> z
-> RTypeBV b v c tv r
-> z
efoldReft Bool
bsc c -> [RTypeBV b v c tv r] -> [(b, a)]
cb RTVar tv (RTypeBV b v c tv (NoReftB b)) -> [(b, a)]
dty RTypeBV b v c tv r -> a
g SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z
f PVarBV b v (RTypeBV b v c tv (NoReftB b)) -> SEnvB b a -> SEnvB b a
fp = SEnvB b a -> z -> RTypeBV b v c tv r -> z
go
  where
    -- folding over RType
    go :: SEnvB b a -> z -> RTypeBV b v c tv r -> z
go SEnvB b a
γ z
z me :: RTypeBV b v c tv r
me@(RVar tv
_ r
r)                = SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z
f SEnvB b a
γ (RTypeBV b v c tv r -> Maybe (RTypeBV b v c tv r)
forall a. a -> Maybe a
Just RTypeBV b v c tv r
me) r
r z
z
    go SEnvB b a
γ z
z me :: RTypeBV b v c tv r
me@(RAllT RTVar tv (RTypeBV b v c tv (NoReftB b))
a RTypeBV b v c tv r
t r
r)
       | RTVar tv (RTypeBV b v c tv (NoReftB b)) -> Bool
forall tv s. RTVar tv s -> Bool
tyVarIsVal RTVar tv (RTypeBV b v c tv (NoReftB b))
a                   = SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z
f SEnvB b a
γ (RTypeBV b v c tv r -> Maybe (RTypeBV b v c tv r)
forall a. a -> Maybe a
Just RTypeBV b v c tv r
me) r
r (SEnvB b a -> z -> RTypeBV b v c tv r -> z
go (SEnvB b a -> [(b, a)] -> SEnvB b a
forall b a.
(Eq b, Hashable b) =>
SEnvB b a -> [(b, a)] -> SEnvB b a
insertsSEnv SEnvB b a
γ (RTVar tv (RTypeBV b v c tv (NoReftB b)) -> [(b, a)]
dty RTVar tv (RTypeBV b v c tv (NoReftB b))
a)) z
z RTypeBV b v c tv r
t)
       | Bool
otherwise                      = SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z
f SEnvB b a
γ (RTypeBV b v c tv r -> Maybe (RTypeBV b v c tv r)
forall a. a -> Maybe a
Just RTypeBV b v c tv r
me) r
r (SEnvB b a -> z -> RTypeBV b v c tv r -> z
go SEnvB b a
γ z
z RTypeBV b v c tv r
t)
    go SEnvB b a
γ z
z (RAllP PVarBV b v (RTypeBV b v c tv (NoReftB b))
p RTypeBV b v c tv r
t)                  = SEnvB b a -> z -> RTypeBV b v c tv r -> z
go (PVarBV b v (RTypeBV b v c tv (NoReftB b)) -> SEnvB b a -> SEnvB b a
fp PVarBV b v (RTypeBV b v c tv (NoReftB b))
p SEnvB b a
γ) z
z RTypeBV b v c tv r
t
    go SEnvB b a
γ z
z me :: RTypeBV b v c tv r
me@(RFun b
_ RFInfo{permitTC :: RFInfo -> Maybe Bool
permitTC = Maybe Bool
permitTC} (RApp c
c [RTypeBV b v c tv r]
ts [RTPropBV b v c tv r]
_ r
_) RTypeBV b v c tv r
t' r
r)
       | (if Maybe Bool
permitTC Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True then c -> Bool
forall c. TyConable c => c -> Bool
isEmbeddedDict else c -> Bool
forall c. TyConable c => c -> Bool
isClass)
         c
c  = SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z
f SEnvB b a
γ (RTypeBV b v c tv r -> Maybe (RTypeBV b v c tv r)
forall a. a -> Maybe a
Just RTypeBV b v c tv r
me) r
r (SEnvB b a -> z -> RTypeBV b v c tv r -> z
go (SEnvB b a -> [(b, a)] -> SEnvB b a
forall b a.
(Eq b, Hashable b) =>
SEnvB b a -> [(b, a)] -> SEnvB b a
insertsSEnv SEnvB b a
γ (c -> [RTypeBV b v c tv r] -> [(b, a)]
cb c
c [RTypeBV b v c tv r]
ts)) (SEnvB b a -> z -> [RTypeBV b v c tv r] -> z
go' SEnvB b a
γ z
z [RTypeBV b v c tv r]
ts) RTypeBV b v c tv r
t')
    go SEnvB b a
γ z
z me :: RTypeBV b v c tv r
me@(RFun b
x RFInfo
_ RTypeBV b v c tv r
t RTypeBV b v c tv r
t' r
r)         = SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z
f SEnvB b a
γ (RTypeBV b v c tv r -> Maybe (RTypeBV b v c tv r)
forall a. a -> Maybe a
Just RTypeBV b v c tv r
me) r
r (SEnvB b a -> z -> RTypeBV b v c tv r -> z
go SEnvB b a
γ' (SEnvB b a -> z -> RTypeBV b v c tv r -> z
go SEnvB b a
γ z
z RTypeBV b v c tv r
t) RTypeBV b v c tv r
t')
       where
         γ' :: SEnvB b a
γ'                             = b -> a -> SEnvB b a -> SEnvB b a
forall b a. (Eq b, Hashable b) => b -> a -> SEnvB b a -> SEnvB b a
insertSEnv b
x (RTypeBV b v c tv r -> a
g RTypeBV b v c tv r
t) SEnvB b a
γ
    go SEnvB b a
γ z
z me :: RTypeBV b v c tv r
me@(RApp c
_ [RTypeBV b v c tv r]
ts [RTPropBV b v c tv r]
rs r
r)          = SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z
f SEnvB b a
γ (RTypeBV b v c tv r -> Maybe (RTypeBV b v c tv r)
forall a. a -> Maybe a
Just RTypeBV b v c tv r
me) r
r (SEnvB b a -> z -> [RTPropBV b v c tv r] -> z
ho' SEnvB b a
γ (SEnvB b a -> z -> [RTypeBV b v c tv r] -> z
go' SEnvB b a
γ' z
z [RTypeBV b v c tv r]
ts) [RTPropBV b v c tv r]
rs)
       where γ' :: SEnvB b a
γ' = if Bool
bsc then b -> a -> SEnvB b a -> SEnvB b a
forall b a. (Eq b, Hashable b) => b -> a -> SEnvB b a -> SEnvB b a
insertSEnv (RTypeBV b v c tv r -> ReftBind r
forall r b v c tv.
(ToReft r, Binder (ReftBind r)) =>
RTypeBV b v c tv r -> ReftBind r
rTypeValueVar RTypeBV b v c tv r
me) (RTypeBV b v c tv r -> a
g RTypeBV b v c tv r
me) SEnvB b a
γ else SEnvB b a
γ

    go SEnvB b a
γ z
z (RAllE b
x RTypeBV b v c tv r
t RTypeBV b v c tv r
t')               = SEnvB b a -> z -> RTypeBV b v c tv r -> z
go (b -> a -> SEnvB b a -> SEnvB b a
forall b a. (Eq b, Hashable b) => b -> a -> SEnvB b a -> SEnvB b a
insertSEnv b
x (RTypeBV b v c tv r -> a
g RTypeBV b v c tv r
t) SEnvB b a
γ) (SEnvB b a -> z -> RTypeBV b v c tv r -> z
go SEnvB b a
γ z
z RTypeBV b v c tv r
t) RTypeBV b v c tv r
t'
    go SEnvB b a
γ z
z (REx b
x RTypeBV b v c tv r
t RTypeBV b v c tv r
t')                 = SEnvB b a -> z -> RTypeBV b v c tv r -> z
go (b -> a -> SEnvB b a -> SEnvB b a
forall b a. (Eq b, Hashable b) => b -> a -> SEnvB b a -> SEnvB b a
insertSEnv b
x (RTypeBV b v c tv r -> a
g RTypeBV b v c tv r
t) SEnvB b a
γ) (SEnvB b a -> z -> RTypeBV b v c tv r -> z
go SEnvB b a
γ z
z RTypeBV b v c tv r
t) RTypeBV b v c tv r
t'
    go SEnvB b a
γ z
z me :: RTypeBV b v c tv r
me@(RRTy [] r
r Oblig
_ RTypeBV b v c tv r
t)           = SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z
f SEnvB b a
γ (RTypeBV b v c tv r -> Maybe (RTypeBV b v c tv r)
forall a. a -> Maybe a
Just RTypeBV b v c tv r
me) r
r (SEnvB b a -> z -> RTypeBV b v c tv r -> z
go SEnvB b a
γ z
z RTypeBV b v c tv r
t)
    go SEnvB b a
γ z
z me :: RTypeBV b v c tv r
me@(RRTy [(b, RTypeBV b v c tv r)]
xts r
r Oblig
_ RTypeBV b v c tv r
t)          = SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z
f SEnvB b a
γ (RTypeBV b v c tv r -> Maybe (RTypeBV b v c tv r)
forall a. a -> Maybe a
Just RTypeBV b v c tv r
me) r
r (SEnvB b a -> z -> RTypeBV b v c tv r -> z
go SEnvB b a
γ (SEnvB b a -> z -> RTypeBV b v c tv r -> z
go SEnvB b a
γ z
z ([(b, RTypeBV b v c tv r)] -> RTypeBV b v c tv r
forall {r} {b} {v} {c} {tv}.
IsReft r =>
[(b, RTypeBV b v c tv r)] -> RTypeBV b v c tv r
envtoType [(b, RTypeBV b v c tv r)]
xts)) RTypeBV b v c tv r
t)
    go SEnvB b a
γ z
z me :: RTypeBV b v c tv r
me@(RAppTy RTypeBV b v c tv r
t RTypeBV b v c tv r
t' r
r)           = SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z
f SEnvB b a
γ (RTypeBV b v c tv r -> Maybe (RTypeBV b v c tv r)
forall a. a -> Maybe a
Just RTypeBV b v c tv r
me) r
r (SEnvB b a -> z -> RTypeBV b v c tv r -> z
go SEnvB b a
γ (SEnvB b a -> z -> RTypeBV b v c tv r -> z
go SEnvB b a
γ z
z RTypeBV b v c tv r
t) RTypeBV b v c tv r
t')
    go SEnvB b a
_ z
z (RExprArg Located (ExprBV b v)
_)                 = z
z
    go SEnvB b a
γ z
z me :: RTypeBV b v c tv r
me@(RHole r
r)                 = SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z
f SEnvB b a
γ (RTypeBV b v c tv r -> Maybe (RTypeBV b v c tv r)
forall a. a -> Maybe a
Just RTypeBV b v c tv r
me) r
r z
z

    -- folding over Ref
    ho :: SEnvB b a -> z -> RTPropBV b v c tv r -> z
ho  SEnvB b a
γ z
z (RProp [(b, RTypeBV b v c tv (NoReftB b))]
ss (RHole r
r))       = SEnvB b a -> Maybe (RTypeBV b v c tv r) -> r -> z -> z
f (SEnvB b a -> [(b, a)] -> SEnvB b a
forall b a.
(Eq b, Hashable b) =>
SEnvB b a -> [(b, a)] -> SEnvB b a
insertsSEnv SEnvB b a
γ ((RTypeBV b v c tv (NoReftB b) -> a)
-> (b, RTypeBV b v c tv (NoReftB b)) -> (b, a)
forall a b. (a -> b) -> (b, a) -> (b, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RTypeBV b v c tv r -> a
g (RTypeBV b v c tv r -> a)
-> (RTypeBV b v c tv (NoReftB b) -> RTypeBV b v c tv r)
-> RTypeBV b v c tv (NoReftB b)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV b v c tv (NoReftB b) -> RTypeBV b v c tv r
forall r b v c tv.
IsReft r =>
RTypeBV b v c tv (NoReftB b) -> RTypeBV b v c tv r
ofRSort) ((b, RTypeBV b v c tv (NoReftB b)) -> (b, a))
-> [(b, RTypeBV b v c tv (NoReftB b))] -> [(b, a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(b, RTypeBV b v c tv (NoReftB b))]
ss)) Maybe (RTypeBV b v c tv r)
forall a. Maybe a
Nothing r
r z
z
    ho  SEnvB b a
γ z
z (RProp [(b, RTypeBV b v c tv (NoReftB b))]
ss RTypeBV b v c tv r
t)               = SEnvB b a -> z -> RTypeBV b v c tv r -> z
go (SEnvB b a -> [(b, a)] -> SEnvB b a
forall b a.
(Eq b, Hashable b) =>
SEnvB b a -> [(b, a)] -> SEnvB b a
insertsSEnv SEnvB b a
γ ((RTypeBV b v c tv (NoReftB b) -> a)
-> (b, RTypeBV b v c tv (NoReftB b)) -> (b, a)
forall a b. (a -> b) -> (b, a) -> (b, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RTypeBV b v c tv r -> a
g (RTypeBV b v c tv r -> a)
-> (RTypeBV b v c tv (NoReftB b) -> RTypeBV b v c tv r)
-> RTypeBV b v c tv (NoReftB b)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV b v c tv (NoReftB b) -> RTypeBV b v c tv r
forall r b v c tv.
IsReft r =>
RTypeBV b v c tv (NoReftB b) -> RTypeBV b v c tv r
ofRSort) ((b, RTypeBV b v c tv (NoReftB b)) -> (b, a))
-> [(b, RTypeBV b v c tv (NoReftB b))] -> [(b, a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(b, RTypeBV b v c tv (NoReftB b))]
ss)) z
z RTypeBV b v c tv r
t

    -- folding over [RType]
    go' :: SEnvB b a -> z -> [RTypeBV b v c tv r] -> z
go' SEnvB b a
γ z
z [RTypeBV b v c tv r]
ts                 = (RTypeBV b v c tv r -> z -> z) -> z -> [RTypeBV b v c tv r] -> z
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((z -> RTypeBV b v c tv r -> z) -> RTypeBV b v c tv r -> z -> z
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((z -> RTypeBV b v c tv r -> z) -> RTypeBV b v c tv r -> z -> z)
-> (z -> RTypeBV b v c tv r -> z) -> RTypeBV b v c tv r -> z -> z
forall a b. (a -> b) -> a -> b
$ SEnvB b a -> z -> RTypeBV b v c tv r -> z
go SEnvB b a
γ) z
z [RTypeBV b v c tv r]
ts

    -- folding over [Ref]
    ho' :: SEnvB b a -> z -> [RTPropBV b v c tv r] -> z
ho' SEnvB b a
γ z
z [RTPropBV b v c tv r]
rs                 = (RTPropBV b v c tv r -> z -> z) -> z -> [RTPropBV b v c tv r] -> z
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((z -> RTPropBV b v c tv r -> z) -> RTPropBV b v c tv r -> z -> z
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((z -> RTPropBV b v c tv r -> z) -> RTPropBV b v c tv r -> z -> z)
-> (z -> RTPropBV b v c tv r -> z) -> RTPropBV b v c tv r -> z -> z
forall a b. (a -> b) -> a -> b
$ SEnvB b a -> z -> RTPropBV b v c tv r -> z
ho SEnvB b a
γ) z
z [RTPropBV b v c tv r]
rs

    envtoType :: [(b, RTypeBV b v c tv r)] -> RTypeBV b v c tv r
envtoType [(b, RTypeBV b v c tv r)]
xts = ((b, RTypeBV b v c tv r)
 -> RTypeBV b v c tv r -> RTypeBV b v c tv r)
-> RTypeBV b v c tv r
-> [(b, RTypeBV b v c tv r)]
-> RTypeBV b v c tv r
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(b
x,RTypeBV b v c tv r
t1) RTypeBV b v c tv r
t2 -> b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
forall r b v c tv.
IsReft r =>
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
rFun b
x RTypeBV b v c tv r
t1 RTypeBV b v c tv r
t2) ((b, RTypeBV b v c tv r) -> RTypeBV b v c tv r
forall a b. (a, b) -> b
snd ((b, RTypeBV b v c tv r) -> RTypeBV b v c tv r)
-> (b, RTypeBV b v c tv r) -> RTypeBV b v c tv r
forall a b. (a -> b) -> a -> b
$ [(b, RTypeBV b v c tv r)] -> (b, RTypeBV b v c tv r)
forall a. HasCallStack => [a] -> a
last [(b, RTypeBV b v c tv r)]
xts) ([(b, RTypeBV b v c tv r)] -> [(b, RTypeBV b v c tv r)]
forall a. HasCallStack => [a] -> [a]
init [(b, RTypeBV b v c tv r)]
xts)

mapRFInfo :: (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo :: forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f (RAllT RTVUBV Symbol Symbol c tv
α RTypeBV Symbol Symbol c tv r
t r
r)     = RTVUBV Symbol Symbol c tv
-> RTypeBV Symbol Symbol c tv r
-> r
-> RTypeBV Symbol Symbol c tv r
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 RTVUBV Symbol Symbol c tv
α ((RFInfo -> RFInfo)
-> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeBV Symbol Symbol c tv r
t) r
r
mapRFInfo RFInfo -> RFInfo
f (RAllP PVUBV Symbol Symbol c tv
π RTypeBV Symbol Symbol c tv r
t)       = PVUBV Symbol Symbol c tv
-> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP PVUBV Symbol Symbol c tv
π ((RFInfo -> RFInfo)
-> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeBV Symbol Symbol c tv r
t)
mapRFInfo RFInfo -> RFInfo
f (RFun Symbol
x RFInfo
i RTypeBV Symbol Symbol c tv r
t RTypeBV Symbol Symbol c tv r
t' r
r) = Symbol
-> RFInfo
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
-> r
-> RTypeBV Symbol Symbol c tv r
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
x (RFInfo -> RFInfo
f RFInfo
i) ((RFInfo -> RFInfo)
-> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeBV Symbol Symbol c tv r
t) ((RFInfo -> RFInfo)
-> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeBV Symbol Symbol c tv r
t') r
r
mapRFInfo RFInfo -> RFInfo
f (RAppTy RTypeBV Symbol Symbol c tv r
t RTypeBV Symbol Symbol c tv r
t' r
r)   = RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
-> r
-> RTypeBV Symbol Symbol c tv r
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 ((RFInfo -> RFInfo)
-> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeBV Symbol Symbol c tv r
t) ((RFInfo -> RFInfo)
-> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeBV Symbol Symbol c tv r
t') r
r
mapRFInfo RFInfo -> RFInfo
f (RApp c
c [RTypeBV Symbol Symbol c tv r]
ts [RTPropBV Symbol Symbol c tv r]
rs r
r)  = c
-> [RTypeBV Symbol Symbol c tv r]
-> [RTPropBV Symbol Symbol c tv r]
-> r
-> RTypeBV Symbol Symbol c tv r
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 c
c ((RFInfo -> RFInfo)
-> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f (RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r)
-> [RTypeBV Symbol Symbol c tv r] -> [RTypeBV Symbol Symbol c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeBV Symbol Symbol c tv r]
ts) ((RFInfo -> RFInfo)
-> RTPropBV Symbol Symbol c tv r -> RTPropBV Symbol Symbol c tv r
forall τ c tv r.
(RFInfo -> RFInfo) -> Ref τ (RType c tv r) -> Ref τ (RType c tv r)
mapRFInfoRef RFInfo -> RFInfo
f (RTPropBV Symbol Symbol c tv r -> RTPropBV Symbol Symbol c tv r)
-> [RTPropBV Symbol Symbol c tv r]
-> [RTPropBV Symbol Symbol c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropBV Symbol Symbol c tv r]
rs) r
r
mapRFInfo RFInfo -> RFInfo
f (REx Symbol
b RTypeBV Symbol Symbol c tv r
t1 RTypeBV Symbol Symbol c tv r
t2)     = Symbol
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
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  ((RFInfo -> RFInfo)
-> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeBV Symbol Symbol c tv r
t1) ((RFInfo -> RFInfo)
-> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeBV Symbol Symbol c tv r
t2)
mapRFInfo RFInfo -> RFInfo
f (RAllE Symbol
b RTypeBV Symbol Symbol c tv r
t1 RTypeBV Symbol Symbol c tv r
t2)   = Symbol
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
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 ((RFInfo -> RFInfo)
-> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeBV Symbol Symbol c tv r
t1) ((RFInfo -> RFInfo)
-> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeBV Symbol Symbol c tv r
t2)
mapRFInfo RFInfo -> RFInfo
f (RRTy [(Symbol, RTypeBV Symbol Symbol c tv r)]
e r
r Oblig
o RTypeBV Symbol Symbol c tv r
t)    = [(Symbol, RTypeBV Symbol Symbol c tv r)]
-> r
-> Oblig
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
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 ((RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r)
-> (Symbol, RTypeBV Symbol Symbol c tv r)
-> (Symbol, RTypeBV Symbol Symbol c tv r)
forall a b. (a -> b) -> (Symbol, a) -> (Symbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((RFInfo -> RFInfo)
-> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f) ((Symbol, RTypeBV Symbol Symbol c tv r)
 -> (Symbol, RTypeBV Symbol Symbol c tv r))
-> [(Symbol, RTypeBV Symbol Symbol c tv r)]
-> [(Symbol, RTypeBV Symbol Symbol c tv r)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RTypeBV Symbol Symbol c tv r)]
e) r
r Oblig
o ((RFInfo -> RFInfo)
-> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeBV Symbol Symbol c tv r
t)
mapRFInfo RFInfo -> RFInfo
_ RTypeBV Symbol Symbol c tv r
t'                = RTypeBV Symbol Symbol c tv r
t'

mapRFInfoRef :: (RFInfo -> RFInfo)
          -> Ref τ (RType c tv r) -> Ref τ (RType c tv r)
mapRFInfoRef :: forall τ c tv r.
(RFInfo -> RFInfo) -> Ref τ (RType c tv r) -> Ref τ (RType c tv r)
mapRFInfoRef RFInfo -> RFInfo
_ (RProp [(Symbol, τ)]
s (RHole r
r)) = [(Symbol, τ)] -> RType c tv r -> RefB Symbol τ (RType c tv r)
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(Symbol, τ)]
s (RType c tv r -> RefB Symbol τ (RType c tv r))
-> RType c tv r -> RefB Symbol τ (RType c tv r)
forall a b. (a -> b) -> a -> b
$ r -> RType c tv r
forall b v c tv r. r -> RTypeBV b v c tv r
RHole r
r
mapRFInfoRef RFInfo -> RFInfo
f (RProp [(Symbol, τ)]
s RType c tv r
t)    = [(Symbol, τ)] -> RType c tv r -> RefB Symbol τ (RType c tv r)
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp  [(Symbol, τ)]
s (RType c tv r -> RefB Symbol τ (RType c tv r))
-> RType c tv r -> RefB Symbol τ (RType c tv r)
forall a b. (a -> b) -> a -> b
$ (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RType c tv r
t

mapBot :: (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot :: forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot RType c tv r -> RType c tv r
f (RAllT RTVUBV Symbol Symbol c tv
α RType c tv r
t r
r)     = RTVUBV Symbol Symbol c tv -> RType c tv r -> r -> RType c tv r
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 RTVUBV Symbol Symbol c tv
α ((RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot RType c tv r -> RType c tv r
f RType c tv r
t) r
r
mapBot RType c tv r -> RType c tv r
f (RAllP PVUBV Symbol Symbol c tv
π RType c tv r
t)       = PVUBV Symbol Symbol c tv -> RType c tv r -> RType c tv r
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP PVUBV Symbol Symbol c tv
π ((RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot RType c tv r -> RType c tv r
f RType c tv r
t)
mapBot RType c tv r -> RType c tv r
f (RFun Symbol
x RFInfo
i RType c tv r
t RType c tv r
t' r
r) = Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
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
x RFInfo
i ((RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot RType c tv r -> RType c tv r
f RType c tv r
t) ((RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot RType c tv r -> RType c tv r
f RType c tv r
t') r
r
mapBot RType c tv r -> RType c tv r
f (RAppTy RType c tv r
t RType c tv r
t' r
r)   = RType c tv r -> RType c tv r -> r -> RType c tv r
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 ((RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot RType c tv r -> RType c tv r
f RType c tv r
t) ((RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot RType c tv r -> RType c tv r
f RType c tv r
t') r
r
mapBot RType c tv r -> RType c tv r
f (RApp c
c [RType c tv r]
ts [RTPropBV Symbol Symbol c tv r]
rs r
r)  = RType c tv r -> RType c tv r
f (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall a b. (a -> b) -> a -> b
$ c
-> [RType c tv r]
-> [RTPropBV Symbol Symbol c tv r]
-> r
-> RType c tv r
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 c
c ((RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot RType c tv r -> RType c tv r
f (RType c tv r -> RType c tv r) -> [RType c tv r] -> [RType c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RType c tv r]
ts) ((RType c tv r -> RType c tv r)
-> RTPropBV Symbol Symbol c tv r -> RTPropBV Symbol Symbol c tv r
forall c tv r τ.
(RType c tv r -> RType c tv r)
-> Ref τ (RType c tv r) -> Ref τ (RType c tv r)
mapBotRef RType c tv r -> RType c tv r
f (RTPropBV Symbol Symbol c tv r -> RTPropBV Symbol Symbol c tv r)
-> [RTPropBV Symbol Symbol c tv r]
-> [RTPropBV Symbol Symbol c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropBV Symbol Symbol c tv r]
rs) r
r
mapBot RType c tv r -> RType c tv r
f (REx Symbol
b RType c tv r
t1 RType c tv r
t2)     = Symbol -> RType c tv r -> RType c tv r -> RType c tv r
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  ((RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot RType c tv r -> RType c tv r
f RType c tv r
t1) ((RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot RType c tv r -> RType c tv r
f RType c tv r
t2)
mapBot RType c tv r -> RType c tv r
f (RAllE Symbol
b RType c tv r
t1 RType c tv r
t2)   = Symbol -> RType c tv r -> RType c tv r -> RType c tv r
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  ((RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot RType c tv r -> RType c tv r
f RType c tv r
t1) ((RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot RType c tv r -> RType c tv r
f RType c tv r
t2)
mapBot RType c tv r -> RType c tv r
f (RRTy [(Symbol, RType c tv r)]
e r
r Oblig
o RType c tv r
t)    = [(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
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 ((RType c tv r -> RType c tv r)
-> (Symbol, RType c tv r) -> (Symbol, RType c tv r)
forall a b. (a -> b) -> (Symbol, a) -> (Symbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot RType c tv r -> RType c tv r
f) ((Symbol, RType c tv r) -> (Symbol, RType c tv r))
-> [(Symbol, RType c tv r)] -> [(Symbol, RType c tv r)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv r)]
e) r
r Oblig
o ((RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot RType c tv r -> RType c tv r
f RType c tv r
t)
mapBot RType c tv r -> RType c tv r
f RType c tv r
t'                = RType c tv r -> RType c tv r
f RType c tv r
t'

mapBotRef :: (RType c tv r -> RType c tv r)
          -> Ref τ (RType c tv r) -> Ref τ (RType c tv r)
mapBotRef :: forall c tv r τ.
(RType c tv r -> RType c tv r)
-> Ref τ (RType c tv r) -> Ref τ (RType c tv r)
mapBotRef RType c tv r -> RType c tv r
_ (RProp [(Symbol, τ)]
s (RHole r
r)) = [(Symbol, τ)] -> RType c tv r -> RefB Symbol τ (RType c tv r)
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(Symbol, τ)]
s (RType c tv r -> RefB Symbol τ (RType c tv r))
-> RType c tv r -> RefB Symbol τ (RType c tv r)
forall a b. (a -> b) -> a -> b
$ r -> RType c tv r
forall b v c tv r. r -> RTypeBV b v c tv r
RHole r
r
mapBotRef RType c tv r -> RType c tv r
f (RProp [(Symbol, τ)]
s RType c tv r
t)         = [(Symbol, τ)] -> RType c tv r -> RefB Symbol τ (RType c tv r)
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(Symbol, τ)]
s (RType c tv r -> RefB Symbol τ (RType c tv r))
-> RType c tv r -> RefB Symbol τ (RType c tv r)
forall a b. (a -> b) -> a -> b
$ (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot RType c tv r -> RType c tv r
f RType c tv r
t

mapBind :: (Hashable b, Hashable b') => (b -> b') -> RTypeBV b v c tv r -> RTypeBV b' v c tv r
mapBind :: forall b b' v c tv r.
(Hashable b, Hashable b') =>
(b -> b') -> RTypeBV b v c tv r -> RTypeBV b' v c tv r
mapBind b -> b'
f = RTypeBV b v c tv r -> RTypeBV b' v c tv r
go
  where
    go :: RTypeBV b v c tv r -> RTypeBV b' v c tv r
go (RAllT RTVUBV b v c tv
α RTypeBV b v c tv r
t r
r)      = RTVUBV b' v c tv -> RTypeBV b' v c tv r -> r -> RTypeBV b' v c tv r
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 (RTVUBV b v c tv -> RTVUBV b' v c tv
mapT RTVUBV b v c tv
α) (RTypeBV b v c tv r -> RTypeBV b' v c tv r
go RTypeBV b v c tv r
t) r
r
    go (RAllP PVUBV b v c tv
π RTypeBV b v c tv r
t)        = PVUBV b' v c tv -> RTypeBV b' v c tv r -> RTypeBV b' v c tv r
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP (PVUBV b v c tv -> PVUBV b' v c tv
mapP PVUBV b v c tv
π) (RTypeBV b v c tv r -> RTypeBV b' v c tv r
go RTypeBV b v c tv r
t)
    go (RFun b
b RFInfo
i RTypeBV b v c tv r
t1 RTypeBV b v c tv r
t2 r
r) = b'
-> RFInfo
-> RTypeBV b' v c tv r
-> RTypeBV b' v c tv r
-> r
-> RTypeBV b' v c tv r
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 (b -> b'
f b
b) RFInfo
i (RTypeBV b v c tv r -> RTypeBV b' v c tv r
go RTypeBV b v c tv r
t1) (RTypeBV b v c tv r -> RTypeBV b' v c tv r
go RTypeBV b v c tv r
t2) r
r
    go (RApp c
c [RTypeBV b v c tv r]
ts [RTPropBV b v c tv r]
rs r
r)   = c
-> [RTypeBV b' v c tv r]
-> [RTPropBV b' v c tv r]
-> r
-> RTypeBV b' v c tv r
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 c
c (RTypeBV b v c tv r -> RTypeBV b' v c tv r
go (RTypeBV b v c tv r -> RTypeBV b' v c tv r)
-> [RTypeBV b v c tv r] -> [RTypeBV b' v c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeBV b v c tv r]
ts) (RTPropBV b v c tv r -> RTPropBV b' v c tv r
mapR (RTPropBV b v c tv r -> RTPropBV b' v c tv r)
-> [RTPropBV b v c tv r] -> [RTPropBV b' v c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropBV b v c tv r]
rs) r
r
    go (RAllE b
b RTypeBV b v c tv r
t1 RTypeBV b v c tv r
t2)    = b'
-> RTypeBV b' v c tv r
-> RTypeBV b' v c tv r
-> RTypeBV b' v c tv r
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  (b -> b'
f b
b) (RTypeBV b v c tv r -> RTypeBV b' v c tv r
go RTypeBV b v c tv r
t1) (RTypeBV b v c tv r -> RTypeBV b' v c tv r
go RTypeBV b v c tv r
t2)
    go (REx b
b RTypeBV b v c tv r
t1 RTypeBV b v c tv r
t2)      = b'
-> RTypeBV b' v c tv r
-> RTypeBV b' v c tv r
-> RTypeBV b' v c tv r
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    (b -> b'
f b
b) (RTypeBV b v c tv r -> RTypeBV b' v c tv r
go RTypeBV b v c tv r
t1) (RTypeBV b v c tv r -> RTypeBV b' v c tv r
go RTypeBV b v c tv r
t2)
    go (RVar tv
α r
r)         = tv -> r -> RTypeBV b' v c tv r
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar tv
α r
r
    go (RHole r
r)          = r -> RTypeBV b' v c tv r
forall b v c tv r. r -> RTypeBV b v c tv r
RHole r
r
    go (RRTy [(b, RTypeBV b v c tv r)]
e r
r Oblig
o RTypeBV b v c tv r
t)     = [(b', RTypeBV b' v c tv r)]
-> r -> Oblig -> RTypeBV b' v c tv r -> RTypeBV b' v c tv r
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 ((b -> b')
-> (RTypeBV b v c tv r -> RTypeBV b' v c tv r)
-> (b, RTypeBV b v c tv r)
-> (b', RTypeBV b' v c tv r)
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 b -> b'
f RTypeBV b v c tv r -> RTypeBV b' v c tv r
go ((b, RTypeBV b v c tv r) -> (b', RTypeBV b' v c tv r))
-> [(b, RTypeBV b v c tv r)] -> [(b', RTypeBV b' v c tv r)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(b, RTypeBV b v c tv r)]
e) r
r Oblig
o (RTypeBV b v c tv r -> RTypeBV b' v c tv r
go RTypeBV b v c tv r
t)
    go (RExprArg Located (ExprBV b v)
e)       = Located (ExprBV b' v) -> RTypeBV b' v c tv r
forall b v c tv r. Located (ExprBV b v) -> RTypeBV b v c tv r
RExprArg ((b -> b') -> ExprBV b v -> ExprBV b' v
forall b b' v.
(Hashable b, Hashable b') =>
(b -> b') -> ExprBV b v -> ExprBV b' v
F.mapBindExpr b -> b'
f (ExprBV b v -> ExprBV b' v)
-> Located (ExprBV b v) -> Located (ExprBV b' v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located (ExprBV b v)
e)
    go (RAppTy RTypeBV b v c tv r
t RTypeBV b v c tv r
t' r
r)    = RTypeBV b' v c tv r
-> RTypeBV b' v c tv r -> r -> RTypeBV b' v c tv r
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 b v c tv r -> RTypeBV b' v c tv r
go RTypeBV b v c tv r
t) (RTypeBV b v c tv r -> RTypeBV b' v c tv r
go RTypeBV b v c tv r
t') r
r
    mapT :: RTVUBV b v c tv -> RTVUBV b' v c tv
mapT (RTVar tv
tv RTVInfo (RTypeBV b v c tv (NoReftB b))
i)     = tv -> RTVInfo (RTypeBV b' v c tv (NoReftB b')) -> RTVUBV b' v c tv
forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar tv
tv (RTVInfo (RTypeBV b v c tv (NoReftB b))
-> RTVInfo (RTypeBV b' v c tv (NoReftB b'))
mapI RTVInfo (RTypeBV b v c tv (NoReftB b))
i)
    mapS :: RTypeBV b v c tv (NoReftB b) -> RTypeBV b' v c tv (NoReftB b')
mapS                  = (NoReftB b -> NoReftB b')
-> RTypeBV b' v c tv (NoReftB b) -> RTypeBV b' v c tv (NoReftB b')
forall r1 r2 b v c tv.
(r1 -> r2) -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
mapReft (\NoReftB b
NoReft -> NoReftB b'
forall b. NoReftB b
NoReft) (RTypeBV b' v c tv (NoReftB b) -> RTypeBV b' v c tv (NoReftB b'))
-> (RTypeBV b v c tv (NoReftB b) -> RTypeBV b' v c tv (NoReftB b))
-> RTypeBV b v c tv (NoReftB b)
-> RTypeBV b' v c tv (NoReftB b')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> b')
-> RTypeBV b v c tv (NoReftB b) -> RTypeBV b' v c tv (NoReftB b)
forall b b' v c tv r.
(Hashable b, Hashable b') =>
(b -> b') -> RTypeBV b v c tv r -> RTypeBV b' v c tv r
mapBind b -> b'
f
    mapI :: RTVInfo (RTypeBV b v c tv (NoReftB b))
-> RTVInfo (RTypeBV b' v c tv (NoReftB b'))
mapI RTVNoInfo{Bool
rtv_is_pol :: forall s. RTVInfo s -> Bool
rtv_is_pol :: Bool
..}    = RTVNoInfo{Bool
rtv_is_pol :: Bool
rtv_is_pol :: Bool
..}
    mapI RTVInfo{Bool
Symbol
RTypeBV b v c tv (NoReftB b)
rtv_is_pol :: forall s. RTVInfo s -> Bool
rtv_is_val :: forall s. RTVInfo s -> Bool
rtv_kind :: forall s. RTVInfo s -> s
rtv_name :: forall s. RTVInfo s -> Symbol
rtv_name :: Symbol
rtv_kind :: RTypeBV b v c tv (NoReftB b)
rtv_is_val :: Bool
rtv_is_pol :: Bool
..}      = RTVInfo { rtv_kind :: RTypeBV b' v c tv (NoReftB b')
rtv_kind = RTypeBV b v c tv (NoReftB b) -> RTypeBV b' v c tv (NoReftB b')
mapS RTypeBV b v c tv (NoReftB b)
rtv_kind, Bool
Symbol
rtv_is_pol :: Bool
rtv_is_val :: Bool
rtv_name :: Symbol
rtv_name :: Symbol
rtv_is_val :: Bool
rtv_is_pol :: Bool
.. }
    mapP :: PVUBV b v c tv -> PVUBV b' v c tv
mapP (PV b
n RTypeBV b v c tv (NoReftB b)
τ b
a [(RTypeBV b v c tv (NoReftB b), b, ExprBV b v)]
as)    = b'
-> RTypeBV b' v c tv (NoReftB b')
-> b'
-> [(RTypeBV b' v c tv (NoReftB b'), b', ExprBV b' v)]
-> PVUBV b' v c tv
forall b v t. b -> t -> b -> [(t, b, ExprBV b v)] -> PVarBV b v t
PV (b -> b'
f b
n) (RTypeBV b v c tv (NoReftB b) -> RTypeBV b' v c tv (NoReftB b')
mapS RTypeBV b v c tv (NoReftB b)
τ) (b -> b'
f b
a) ((RTypeBV b v c tv (NoReftB b), b, ExprBV b v)
-> (RTypeBV b' v c tv (NoReftB b'), b', ExprBV b' v)
mapA ((RTypeBV b v c tv (NoReftB b), b, ExprBV b v)
 -> (RTypeBV b' v c tv (NoReftB b'), b', ExprBV b' v))
-> [(RTypeBV b v c tv (NoReftB b), b, ExprBV b v)]
-> [(RTypeBV b' v c tv (NoReftB b'), b', ExprBV b' v)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(RTypeBV b v c tv (NoReftB b), b, ExprBV b v)]
as)
    mapA :: (RTypeBV b v c tv (NoReftB b), b, ExprBV b v)
-> (RTypeBV b' v c tv (NoReftB b'), b', ExprBV b' v)
mapA (RTypeBV b v c tv (NoReftB b)
τ, b
b, ExprBV b v
e)        = (RTypeBV b v c tv (NoReftB b) -> RTypeBV b' v c tv (NoReftB b')
mapS RTypeBV b v c tv (NoReftB b)
τ, b -> b'
f b
b, (b -> b') -> ExprBV b v -> ExprBV b' v
forall b b' v.
(Hashable b, Hashable b') =>
(b -> b') -> ExprBV b v -> ExprBV b' v
F.mapBindExpr b -> b'
f ExprBV b v
e)
    mapR :: RTPropBV b v c tv r -> RTPropBV b' v c tv r
mapR (RProp [(b, RTypeBV b v c tv (NoReftB b))]
as RTypeBV b v c tv r
t)     = [(b', RTypeBV b' v c tv (NoReftB b'))]
-> RTypeBV b' v c tv r -> RTPropBV b' v c tv r
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp ((b -> b')
-> (RTypeBV b v c tv (NoReftB b) -> RTypeBV b' v c tv (NoReftB b'))
-> (b, RTypeBV b v c tv (NoReftB b))
-> (b', RTypeBV b' v c tv (NoReftB b'))
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 b -> b'
f RTypeBV b v c tv (NoReftB b) -> RTypeBV b' v c tv (NoReftB b')
mapS ((b, RTypeBV b v c tv (NoReftB b))
 -> (b', RTypeBV b' v c tv (NoReftB b')))
-> [(b, RTypeBV b v c tv (NoReftB b))]
-> [(b', RTypeBV b' v c tv (NoReftB b'))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(b, RTypeBV b v c tv (NoReftB b))]
as) (RTypeBV b v c tv r -> RTypeBV b' v c tv r
go RTypeBV b v c tv r
t)

--------------------------------------------------
ofRSort ::  IsReft r => RTypeBV b v c tv (NoReftB b) -> RTypeBV b v c tv r
ofRSort :: forall r b v c tv.
IsReft r =>
RTypeBV b v c tv (NoReftB b) -> RTypeBV b v c tv r
ofRSort = (NoReftB b -> r)
-> RTypeBV b v c tv (NoReftB b) -> RTypeBV b v c tv r
forall a b. (a -> b) -> RTypeBV b v c tv a -> RTypeBV b v c tv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (r -> NoReftB b -> r
forall a b. a -> b -> a
const r
forall r. IsReft r => r
trueReft)

toRSort :: F.Binder b => RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort :: forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort = RTypeBV b v c tv (NoReftB b) -> RTypeBV b v c tv (NoReftB b)
forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
stripAnnotations (RTypeBV b v c tv (NoReftB b) -> RTypeBV b v c tv (NoReftB b))
-> (RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b))
-> RTypeBV b v c tv r
-> RTypeBV b v c tv (NoReftB b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> b)
-> RTypeBV b v c tv (NoReftB b) -> RTypeBV b v c tv (NoReftB b)
forall b b' v c tv r.
(Hashable b, Hashable b') =>
(b -> b') -> RTypeBV b v c tv r -> RTypeBV b' v c tv r
mapBind (b -> b -> b
forall a b. a -> b -> a
const b
forall b. Binder b => b
F.wildcard) (RTypeBV b v c tv (NoReftB b) -> RTypeBV b v c tv (NoReftB b))
-> (RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b))
-> RTypeBV b v c tv r
-> RTypeBV b v c tv (NoReftB b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NoReftB b
forall b. NoReftB b
NoReft NoReftB b -> RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
forall a b. a -> RTypeBV b v c tv b -> RTypeBV b v c tv a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$)

stripAnnotations :: RTypeBV b v c tv r -> RTypeBV b v c tv r
stripAnnotations :: forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
stripAnnotations (RAllT RTVUBV b v c tv
α RTypeBV b v c tv r
t r
r)     = RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
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 RTVUBV b v c tv
α (RTypeBV b v c tv r -> RTypeBV b v c tv r
forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
stripAnnotations RTypeBV b v c tv r
t) r
r
stripAnnotations (RAllP PVUBV b v c tv
_ RTypeBV b v c tv r
t)       = RTypeBV b v c tv r -> RTypeBV b v c tv r
forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
stripAnnotations RTypeBV b v c tv r
t
stripAnnotations (RAllE b
_ RTypeBV b v c tv r
_ RTypeBV b v c tv r
t)     = RTypeBV b v c tv r -> RTypeBV b v c tv r
forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
stripAnnotations RTypeBV b v c tv r
t
stripAnnotations (REx b
_ RTypeBV b v c tv r
_ RTypeBV b v c tv r
t)       = RTypeBV b v c tv r -> RTypeBV b v c tv r
forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
stripAnnotations RTypeBV b v c tv r
t
stripAnnotations (RFun b
x RFInfo
i RTypeBV b v c tv r
t RTypeBV b v c tv r
t' r
r) = b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
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 b
x RFInfo
i (RTypeBV b v c tv r -> RTypeBV b v c tv r
forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
stripAnnotations RTypeBV b v c tv r
t) (RTypeBV b v c tv r -> RTypeBV b v c tv r
forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
stripAnnotations RTypeBV b v c tv r
t') r
r
stripAnnotations (RAppTy RTypeBV b v c tv r
t RTypeBV b v c tv r
t' r
r)   = RTypeBV b v c tv r -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
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 b v c tv r -> RTypeBV b v c tv r
forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
stripAnnotations RTypeBV b v c tv r
t) (RTypeBV b v c tv r -> RTypeBV b v c tv r
forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
stripAnnotations RTypeBV b v c tv r
t') r
r
stripAnnotations (RApp c
c [RTypeBV b v c tv r]
ts [RTPropBV b v c tv r]
rs r
r)  = c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
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 c
c (RTypeBV b v c tv r -> RTypeBV b v c tv r
forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
stripAnnotations (RTypeBV b v c tv r -> RTypeBV b v c tv r)
-> [RTypeBV b v c tv r] -> [RTypeBV b v c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeBV b v c tv r]
ts) (RTPropBV b v c tv r -> RTPropBV b v c tv r
forall b τ v c tv r.
RefB b τ (RTypeBV b v c tv r) -> RefB b τ (RTypeBV b v c tv r)
stripAnnotationsRef (RTPropBV b v c tv r -> RTPropBV b v c tv r)
-> [RTPropBV b v c tv r] -> [RTPropBV b v c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropBV b v c tv r]
rs) r
r
stripAnnotations (RRTy [(b, RTypeBV b v c tv r)]
_ r
_ Oblig
_ RTypeBV b v c tv r
t)    = RTypeBV b v c tv r -> RTypeBV b v c tv r
forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
stripAnnotations RTypeBV b v c tv r
t
stripAnnotations RTypeBV b v c tv r
t                 = RTypeBV b v c tv r
t

stripAnnotationsRef :: RefB b τ (RTypeBV b v c tv r) -> RefB b τ (RTypeBV b v c tv r)
stripAnnotationsRef :: forall b τ v c tv r.
RefB b τ (RTypeBV b v c tv r) -> RefB b τ (RTypeBV b v c tv r)
stripAnnotationsRef (RProp [(b, τ)]
s (RHole r
r)) = [(b, τ)] -> RTypeBV b v c tv r -> RefB b τ (RTypeBV b v c tv r)
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(b, τ)]
s (r -> RTypeBV b v c tv r
forall b v c tv r. r -> RTypeBV b v c tv r
RHole r
r)
stripAnnotationsRef (RProp [(b, τ)]
s RTypeBV b v c tv r
t)         = [(b, τ)] -> RTypeBV b v c tv r -> RefB b τ (RTypeBV b v c tv r)
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(b, τ)]
s (RTypeBV b v c tv r -> RefB b τ (RTypeBV b v c tv r))
-> RTypeBV b v c tv r -> RefB b τ (RTypeBV b v c tv r)
forall a b. (a -> b) -> a -> b
$ RTypeBV b v c tv r -> RTypeBV b v c tv r
forall b v c tv r. RTypeBV b v c tv r -> RTypeBV b v c tv r
stripAnnotations RTypeBV b v c tv r
t

insertSEnv :: (Eq b, Hashable b) => b -> a -> F.SEnvB b a -> F.SEnvB b a
insertSEnv :: forall b a. (Eq b, Hashable b) => b -> a -> SEnvB b a -> SEnvB b a
insertSEnv = b -> a -> SEnvB b a -> SEnvB b a
forall b a. Hashable b => b -> a -> SEnvB b a -> SEnvB b a
F.insertSEnv

insertsSEnv :: (Eq b, Hashable b) => F.SEnvB b a -> [(b, a)] -> F.SEnvB b a
insertsSEnv :: forall b a.
(Eq b, Hashable b) =>
SEnvB b a -> [(b, a)] -> SEnvB b a
insertsSEnv  = ((b, a) -> SEnvB b a -> SEnvB b a)
-> SEnvB b a -> [(b, a)] -> SEnvB b a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(b
x, a
t) SEnvB b a
γ -> b -> a -> SEnvB b a -> SEnvB b a
forall b a. (Eq b, Hashable b) => b -> a -> SEnvB b a -> SEnvB b a
insertSEnv b
x a
t SEnvB b a
γ)

rTypeValueVar :: (ToReft r, F.Binder (ReftBind r)) => RTypeBV b v c tv r -> ReftBind r
rTypeValueVar :: forall r b v c tv.
(ToReft r, Binder (ReftBind r)) =>
RTypeBV b v c tv r -> ReftBind r
rTypeValueVar RTypeBV b v c tv r
t = ReftBind r
vv where F.Reft (ReftBind r
vv,ExprBV (ReftBind r) (ReftVar r)
_) =  RTypeBV b v c tv r -> ReftBV (ReftBind r) (ReftVar r)
forall r b v c tv.
(ToReft r, Binder (ReftBind r)) =>
RTypeBV b v c tv r -> ReftBV (ReftBind r) (ReftVar r)
rTypeReft RTypeBV b v c tv r
t

rTypeReft :: (ToReft r, F.Binder (ReftBind r)) => RTypeBV b v c tv r -> F.ReftBV (ReftBind r) (ReftVar r)
rTypeReft :: forall r b v c tv.
(ToReft r, Binder (ReftBind r)) =>
RTypeBV b v c tv r -> ReftBV (ReftBind r) (ReftVar r)
rTypeReft = ReftBV (ReftBind r) (ReftVar r)
-> (r -> ReftBV (ReftBind r) (ReftVar r))
-> Maybe r
-> ReftBV (ReftBind r) (ReftVar r)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ReftBV (ReftBind r) (ReftVar r)
forall b v. Binder b => ReftBV b v
F.trueReft r -> ReftBV (ReftBind r) (ReftVar r)
forall r. ToReft r => r -> ReftBV (ReftBind r) (ReftVar r)
toReft (Maybe r -> ReftBV (ReftBind r) (ReftVar r))
-> (RTypeBV b v c tv r -> Maybe r)
-> RTypeBV b v c tv r
-> ReftBV (ReftBind r) (ReftVar r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV b v c tv r -> Maybe r
forall b v c tv r. RTypeBV b v c tv r -> Maybe r
stripRTypeBase

-- stripRTypeBase ::  RType a -> Maybe a
stripRTypeBase :: RTypeBV b v c tv r -> Maybe r
stripRTypeBase :: forall b v c tv r. RTypeBV b v c tv r -> Maybe r
stripRTypeBase (RApp c
_ [RTypeBV b v c tv r]
_ [RTPropBV b v c tv r]
_ r
x)   = r -> Maybe r
forall a. a -> Maybe a
Just r
x
stripRTypeBase (RVar tv
_ r
x)       = r -> Maybe r
forall a. a -> Maybe a
Just r
x
stripRTypeBase (RFun b
_ RFInfo
_ RTypeBV b v c tv r
_ RTypeBV b v c tv r
_ r
x) = r -> Maybe r
forall a. a -> Maybe a
Just r
x
stripRTypeBase (RAppTy RTypeBV b v c tv r
_ RTypeBV b v c tv r
_ r
x)   = r -> Maybe r
forall a. a -> Maybe a
Just r
x
stripRTypeBase (RAllT RTVUBV b v c tv
_ RTypeBV b v c tv r
_ r
x)    = r -> Maybe r
forall a. a -> Maybe a
Just r
x
stripRTypeBase RTypeBV b v c tv r
_                = Maybe r
forall a. Maybe a
Nothing

topRTypeBase :: (Top r) => RType c tv r -> RType c tv r
topRTypeBase :: forall r c tv. Top r => RType c tv r -> RType c tv r
topRTypeBase = (r -> r) -> RType c tv r -> RType c tv r
forall r c tv. (r -> r) -> RType c tv r -> RType c tv r
mapRBase r -> r
forall r. Top r => r -> r
top

mapRBase :: (r -> r) -> RType c tv r -> RType c tv r
mapRBase :: forall r c tv. (r -> r) -> RType c tv r -> RType c tv r
mapRBase r -> r
f (RApp c
c [RTypeBV Symbol Symbol c tv r]
ts [RTPropBV Symbol Symbol c tv r]
rs r
r)   = c
-> [RTypeBV Symbol Symbol c tv r]
-> [RTPropBV Symbol Symbol c tv r]
-> r
-> RTypeBV Symbol Symbol c tv r
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 c
c [RTypeBV Symbol Symbol c tv r]
ts [RTPropBV Symbol Symbol c tv r]
rs (r -> RTypeBV Symbol Symbol c tv r)
-> r -> RTypeBV Symbol Symbol c tv r
forall a b. (a -> b) -> a -> b
$ r -> r
f r
r
mapRBase r -> r
f (RVar tv
a r
r)         = tv -> r -> RTypeBV Symbol Symbol c tv r
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar tv
a (r -> RTypeBV Symbol Symbol c tv r)
-> r -> RTypeBV Symbol Symbol c tv r
forall a b. (a -> b) -> a -> b
$ r -> r
f r
r
mapRBase r -> r
f (RFun Symbol
x RFInfo
i RTypeBV Symbol Symbol c tv r
t1 RTypeBV Symbol Symbol c tv r
t2 r
r) = Symbol
-> RFInfo
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
-> r
-> RTypeBV Symbol Symbol c tv r
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
x RFInfo
i RTypeBV Symbol Symbol c tv r
t1 RTypeBV Symbol Symbol c tv r
t2 (r -> RTypeBV Symbol Symbol c tv r)
-> r -> RTypeBV Symbol Symbol c tv r
forall a b. (a -> b) -> a -> b
$ r -> r
f r
r
mapRBase r -> r
f (RAppTy RTypeBV Symbol Symbol c tv r
t1 RTypeBV Symbol Symbol c tv r
t2 r
r)   = RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
-> r
-> RTypeBV Symbol Symbol c tv r
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 c tv r
t1 RTypeBV Symbol Symbol c tv r
t2 (r -> RTypeBV Symbol Symbol c tv r)
-> r -> RTypeBV Symbol Symbol c tv r
forall a b. (a -> b) -> a -> b
$ r -> r
f r
r
mapRBase r -> r
_ RTypeBV Symbol Symbol c tv r
t                  = RTypeBV Symbol Symbol c tv r
t