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

{-# 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(..), 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, void)
import           Data.Bifunctor (first)

import qualified Language.Fixpoint.Types as F
import           Language.Fixpoint.Types (Expr, 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
data RTypeRepV v c tv r = RTypeRep
  { forall v c tv r.
RTypeRepV v c tv r -> [(RTVar tv (RTypeV v c tv ()), r)]
ty_vars   :: [(RTVar tv (RTypeV v c tv ()), r)]
  , forall v c tv r. RTypeRepV v c tv r -> [PVarV v (RTypeV v c tv ())]
ty_preds  :: [PVarV v (RTypeV v c tv ())]
  , forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds  :: [Symbol]
  , forall v c tv r. RTypeRepV v c tv r -> [RFInfo]
ty_info   :: [RFInfo]
  , forall v c tv r. RTypeRepV v c tv r -> [r]
ty_refts  :: [r]
  , forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_args   :: [RTypeV v c tv r]
  , forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
ty_res    :: RTypeV v c tv r
  }

fromRTypeRep :: RTypeRepV v c tv r -> RTypeV v c tv r
fromRTypeRep :: forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
fromRTypeRep RTypeRep{[r]
[(RTVar tv (RTypeV v c tv ()), r)]
[Symbol]
[RTypeV v c tv r]
[PVarV v (RTypeV v c tv ())]
[RFInfo]
RTypeV v c tv r
ty_vars :: forall v c tv r.
RTypeRepV v c tv r -> [(RTVar tv (RTypeV v c tv ()), r)]
ty_preds :: forall v c tv r. RTypeRepV v c tv r -> [PVarV v (RTypeV v c tv ())]
ty_binds :: forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_info :: forall v c tv r. RTypeRepV v c tv r -> [RFInfo]
ty_refts :: forall v c tv r. RTypeRepV v c tv r -> [r]
ty_args :: forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_res :: forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
ty_vars :: [(RTVar tv (RTypeV v c tv ()), r)]
ty_preds :: [PVarV v (RTypeV v c tv ())]
ty_binds :: [Symbol]
ty_info :: [RFInfo]
ty_refts :: [r]
ty_args :: [RTypeV v c tv r]
ty_res :: RTypeV v c tv r
..}
  = [(RTVar tv (RTypeV v c tv ()), r)]
-> [PVarV v (RTypeV v c tv ())]
-> [(Symbol, RFInfo, RTypeV v c tv r, r)]
-> RTypeV v c tv r
-> RTypeV v c tv r
forall tv v c r.
[(RTVar tv (RTypeV v c tv ()), r)]
-> [PVarV v (RTypeV v c tv ())]
-> [(Symbol, RFInfo, RTypeV v c tv r, r)]
-> RTypeV v c tv r
-> RTypeV v c tv r
mkArrow [(RTVar tv (RTypeV v c tv ()), r)]
ty_vars [PVarV v (RTypeV v c tv ())]
ty_preds [(Symbol, RFInfo, RTypeV v c tv r, r)]
arrs RTypeV v c tv r
ty_res
  where
    arrs :: [(Symbol, RFInfo, RTypeV v c tv r, r)]
arrs = [Char]
-> [Symbol]
-> [RFInfo]
-> [RTypeV v c tv r]
-> [r]
-> [(Symbol, RFInfo, RTypeV 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 ([Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
ty_binds, [RFInfo] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RFInfo]
ty_info, [RTypeV v c tv r] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RTypeV v c tv r]
ty_args, [r] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [r]
ty_refts)) [Symbol]
ty_binds [RFInfo]
ty_info [RTypeV 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 = RTypeRepV Symbol c tv r -> RTypeV Symbol c tv r
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
fromRTypeRep (RTypeRepV Symbol c tv r -> RTypeV Symbol c tv r)
-> (RTypeV Symbol c tv r -> RTypeRepV Symbol c tv r)
-> RTypeV Symbol c tv r
-> RTypeV Symbol c tv r
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                    (\trep :: RTypeRepV Symbol c tv r
trep@RTypeRep{[r]
[(RTVar tv (RTypeV Symbol c tv ()), r)]
[Symbol]
[RTypeV Symbol c tv r]
[PVarV Symbol (RTypeV Symbol c tv ())]
[RFInfo]
RTypeV Symbol c tv r
ty_vars :: forall v c tv r.
RTypeRepV v c tv r -> [(RTVar tv (RTypeV v c tv ()), r)]
ty_preds :: forall v c tv r. RTypeRepV v c tv r -> [PVarV v (RTypeV v c tv ())]
ty_binds :: forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_info :: forall v c tv r. RTypeRepV v c tv r -> [RFInfo]
ty_refts :: forall v c tv r. RTypeRepV v c tv r -> [r]
ty_args :: forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_res :: forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
ty_vars :: [(RTVar tv (RTypeV Symbol c tv ()), r)]
ty_preds :: [PVarV Symbol (RTypeV Symbol c tv ())]
ty_binds :: [Symbol]
ty_info :: [RFInfo]
ty_refts :: [r]
ty_args :: [RTypeV Symbol c tv r]
ty_res :: RTypeV Symbol c tv r
..} -> RTypeRepV Symbol c tv r
trep{ty_info = map (\RFInfo
i -> RFInfo
i{permitTC = pure b}) ty_info}) (RTypeRepV Symbol c tv r -> RTypeRepV Symbol c tv r)
-> (RTypeV Symbol c tv r -> RTypeRepV Symbol c tv r)
-> RTypeV Symbol c tv r
-> RTypeRepV Symbol c tv r
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                    RTypeV Symbol c tv r -> RTypeRepV Symbol c tv r
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep

--------------------------------------------------------------------------------
toRTypeRep           :: RTypeV v c tv r -> RTypeRepV v c tv r
--------------------------------------------------------------------------------
toRTypeRep :: forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep RTypeV v c tv r
t         = [(RTVar tv (RTypeV v c tv ()), r)]
-> [PVarV v (RTypeV v c tv ())]
-> [Symbol]
-> [RFInfo]
-> [r]
-> [RTypeV v c tv r]
-> RTypeV v c tv r
-> RTypeRepV v c tv r
forall v c tv r.
[(RTVar tv (RTypeV v c tv ()), r)]
-> [PVarV v (RTypeV v c tv ())]
-> [Symbol]
-> [RFInfo]
-> [r]
-> [RTypeV v c tv r]
-> RTypeV v c tv r
-> RTypeRepV v c tv r
RTypeRep [(RTVar tv (RTypeV v c tv ()), r)]
αs [PVarV v (RTypeV v c tv ())]
πs [Symbol]
xs [RFInfo]
is [r]
rs [RTypeV v c tv r]
ts RTypeV v c tv r
t''
  where
    ([(RTVar tv (RTypeV v c tv ()), r)]
αs, [PVarV v (RTypeV v c tv ())]
πs, RTypeV v c tv r
t') = RTypeV v c tv r
-> ([(RTVar tv (RTypeV v c tv ()), r)],
    [PVarV v (RTypeV v c tv ())], RTypeV v c tv r)
forall v tv c r.
RTypeV v tv c r
-> ([(RTVar c (RTypeV v tv c ()), r)],
    [PVarV v (RTypeV v tv c ())], RTypeV v tv c r)
bkUniv RTypeV v c tv r
t
    (([Symbol]
xs, [RFInfo]
is, [RTypeV v c tv r]
ts, [r]
rs), RTypeV v c tv r
t'') = RTypeV v c tv r
-> (([Symbol], [RFInfo], [RTypeV v c tv r], [r]), RTypeV v c tv r)
forall v t t1 a.
RTypeV v t t1 a
-> (([Symbol], [RFInfo], [RTypeV v t t1 a], [a]), RTypeV v t t1 a)
bkArrow RTypeV v c tv r
t'

mkArrow :: [(RTVar tv (RTypeV v c tv ()), r)]
        -> [PVarV v (RTypeV v c tv ())]
        -> [(Symbol, RFInfo, RTypeV v c tv r, r)]
        -> RTypeV v c tv r
        -> RTypeV v c tv r
mkArrow :: forall tv v c r.
[(RTVar tv (RTypeV v c tv ()), r)]
-> [PVarV v (RTypeV v c tv ())]
-> [(Symbol, RFInfo, RTypeV v c tv r, r)]
-> RTypeV v c tv r
-> RTypeV v c tv r
mkArrow [(RTVar tv (RTypeV v c tv ()), r)]
αs [PVarV v (RTypeV v c tv ())]
πs [(Symbol, RFInfo, RTypeV v c tv r, r)]
zts = [(RTVar tv (RTypeV v c tv ()), r)]
-> [PVarV v (RTypeV v c tv ())]
-> RTypeV v c tv r
-> RTypeV v c tv r
forall (t :: * -> *) (t1 :: * -> *) tv v c r.
(Foldable t, Foldable t1) =>
t (RTVar tv (RTypeV v c tv ()), r)
-> t1 (PVarV v (RTypeV v c tv ()))
-> RTypeV v c tv r
-> RTypeV v c tv r
mkUnivs [(RTVar tv (RTypeV v c tv ()), r)]
αs [PVarV v (RTypeV v c tv ())]
πs (RTypeV v c tv r -> RTypeV v c tv r)
-> (RTypeV v c tv r -> RTypeV v c tv r)
-> RTypeV v c tv r
-> RTypeV v c tv r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, RFInfo, RTypeV v c tv r, r)]
-> RTypeV v c tv r -> RTypeV v c tv r
forall {t :: * -> *} {v} {c} {tv} {r}.
Foldable t =>
t (Symbol, RFInfo, RTypeV v c tv r, r)
-> RTypeV v c tv r -> RTypeV v c tv r
mkRFuns [(Symbol, RFInfo, RTypeV v c tv r, r)]
zts
  where
    mkRFuns :: t (Symbol, RFInfo, RTypeV v c tv r, r)
-> RTypeV v c tv r -> RTypeV v c tv r
mkRFuns t (Symbol, RFInfo, RTypeV v c tv r, r)
xts RTypeV v c tv r
t = ((Symbol, RFInfo, RTypeV v c tv r, r)
 -> RTypeV v c tv r -> RTypeV v c tv r)
-> RTypeV v c tv r
-> t (Symbol, RFInfo, RTypeV v c tv r, r)
-> RTypeV 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 (\(Symbol
b,RFInfo
i,RTypeV v c tv r
t1,r
r) RTypeV v c tv r
t2 -> Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
b RFInfo
i RTypeV v c tv r
t1 RTypeV v c tv r
t2 r
r) RTypeV v c tv r
t t (Symbol, RFInfo, RTypeV 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 RTVUV Symbol t t1
_ RTypeV Symbol t t1 a
t a
_)   = RTypeV Symbol t t1 a
-> ([Symbol], [RFInfo], [RTypeV Symbol t t1 a], [a],
    RTypeV Symbol t t1 a)
forall t t1 a.
RType t t1 a
-> ([Symbol], [RFInfo], [RType t t1 a], [a], RType t t1 a)
bkArrowDeep RTypeV Symbol t t1 a
t
bkArrowDeep (RAllP PVUV Symbol t t1
_ RTypeV Symbol t t1 a
t)     = RTypeV Symbol t t1 a
-> ([Symbol], [RFInfo], [RTypeV Symbol t t1 a], [a],
    RTypeV Symbol t t1 a)
forall t t1 a.
RType t t1 a
-> ([Symbol], [RFInfo], [RType t t1 a], [a], RType t t1 a)
bkArrowDeep RTypeV Symbol t t1 a
t
bkArrowDeep (RFun Symbol
x RFInfo
i RTypeV Symbol t t1 a
t RTypeV Symbol t t1 a
t' a
r) = let ([Symbol]
xs, [RFInfo]
is, [RTypeV Symbol t t1 a]
ts, [a]
rs, RTypeV Symbol t t1 a
t'') = RTypeV Symbol t t1 a
-> ([Symbol], [RFInfo], [RTypeV Symbol t t1 a], [a],
    RTypeV Symbol t t1 a)
forall t t1 a.
RType t t1 a
-> ([Symbol], [RFInfo], [RType t t1 a], [a], RType t t1 a)
bkArrowDeep RTypeV 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, RTypeV Symbol t t1 a
tRTypeV Symbol t t1 a
-> [RTypeV Symbol t t1 a] -> [RTypeV Symbol t t1 a]
forall a. a -> [a] -> [a]
:[RTypeV Symbol t t1 a]
ts, a
ra -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
rs, RTypeV Symbol t t1 a
t'')
bkArrowDeep RTypeV Symbol t t1 a
t               = ([], [], [], [], RTypeV Symbol t t1 a
t)

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

bkFun :: RTypeV v t t1 a -> ([Symbol], [RFInfo], [RTypeV v t t1 a], [a], RTypeV v t t1 a)
bkFun :: forall v t t1 a.
RTypeV v t t1 a
-> ([Symbol], [RFInfo], [RTypeV v t t1 a], [a], RTypeV v t t1 a)
bkFun (RFun Symbol
x RFInfo
i RTypeV v t t1 a
t RTypeV v t t1 a
t' a
r) = let ([Symbol]
xs, [RFInfo]
is, [RTypeV v t t1 a]
ts, [a]
rs, RTypeV v t t1 a
t'') = RTypeV v t t1 a
-> ([Symbol], [RFInfo], [RTypeV v t t1 a], [a], RTypeV v t t1 a)
forall v t t1 a.
RTypeV v t t1 a
-> ([Symbol], [RFInfo], [RTypeV v t t1 a], [a], RTypeV v t t1 a)
bkFun RTypeV v 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, RTypeV v t t1 a
tRTypeV v t t1 a -> [RTypeV v t t1 a] -> [RTypeV v t t1 a]
forall a. a -> [a] -> [a]
:[RTypeV v t t1 a]
ts, a
ra -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
rs, RTypeV v t t1 a
t'')
bkFun RTypeV v t t1 a
t                 = ([], [], [], [], RTypeV 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 PVUV 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 v t t1 a.
RTypeV v t t1 a
-> (([Symbol], [RFInfo], [RTypeV v t t1 a], [a]), RTypeV v t t1 a)
bkArrow RType t t1 a
t

mkUnivs :: (Foldable t, Foldable t1)
        => t  (RTVar tv (RTypeV v c tv ()), r)
        -> t1 (PVarV v (RTypeV v c tv ()))
        -> RTypeV v c tv r
        -> RTypeV v c tv r
mkUnivs :: forall (t :: * -> *) (t1 :: * -> *) tv v c r.
(Foldable t, Foldable t1) =>
t (RTVar tv (RTypeV v c tv ()), r)
-> t1 (PVarV v (RTypeV v c tv ()))
-> RTypeV v c tv r
-> RTypeV v c tv r
mkUnivs t (RTVar tv (RTypeV v c tv ()), r)
αs t1 (PVarV v (RTypeV v c tv ()))
πs RTypeV v c tv r
rt = ((RTVar tv (RTypeV v c tv ()), r)
 -> RTypeV v c tv r -> RTypeV v c tv r)
-> RTypeV v c tv r
-> t (RTVar tv (RTypeV v c tv ()), r)
-> RTypeV 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 (RTypeV v c tv ())
a,r
r) RTypeV v c tv r
t -> RTVar tv (RTypeV v c tv ())
-> RTypeV v c tv r -> r -> RTypeV v c tv r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVar tv (RTypeV v c tv ())
a RTypeV v c tv r
t r
r) ((PVarV v (RTypeV v c tv ()) -> RTypeV v c tv r -> RTypeV v c tv r)
-> RTypeV v c tv r
-> t1 (PVarV v (RTypeV v c tv ()))
-> RTypeV 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 PVarV v (RTypeV v c tv ()) -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP RTypeV v c tv r
rt t1 (PVarV v (RTypeV v c tv ()))
πs) t (RTVar tv (RTypeV v c tv ()), 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 v tv c r.
RTypeV v tv c r
-> ([(RTVar c (RTypeV v tv c ()), r)],
    [PVarV v (RTypeV v tv c ())], RTypeV v tv c r)
bkUniv  SpecType
t
    ([(RTyCon, [SpecType])]
cs, SpecType
t2)     = SpecType -> ([(RTyCon, [SpecType])], SpecType)
forall c tv r.
(PPrint c, TyConable c) =>
RType c tv r -> ([(c, [RType c tv r])], RType c tv r)
bkClass SpecType
t1


bkUniv :: RTypeV v tv c r -> ([(RTVar c (RTypeV v tv c ()), r)], [PVarV v (RTypeV v tv c ())], RTypeV v tv c r)
bkUniv :: forall v tv c r.
RTypeV v tv c r
-> ([(RTVar c (RTypeV v tv c ()), r)],
    [PVarV v (RTypeV v tv c ())], RTypeV v tv c r)
bkUniv (RAllT RTVUV v tv c
α RTypeV v tv c r
t r
r) = let ([(RTVUV v tv c, r)]
αs, [PVarV v (RTypeV v tv c ())]
πs, RTypeV v tv c r
t') = RTypeV v tv c r
-> ([(RTVUV v tv c, r)], [PVarV v (RTypeV v tv c ())],
    RTypeV v tv c r)
forall v tv c r.
RTypeV v tv c r
-> ([(RTVar c (RTypeV v tv c ()), r)],
    [PVarV v (RTypeV v tv c ())], RTypeV v tv c r)
bkUniv RTypeV v tv c r
t in ((RTVUV v tv c
α, r
r)(RTVUV v tv c, r) -> [(RTVUV v tv c, r)] -> [(RTVUV v tv c, r)]
forall a. a -> [a] -> [a]
:[(RTVUV v tv c, r)]
αs, [PVarV v (RTypeV v tv c ())]
πs, RTypeV v tv c r
t')
bkUniv (RAllP PVarV v (RTypeV v tv c ())
π RTypeV v tv c r
t)   = let ([(RTVUV v tv c, r)]
αs, [PVarV v (RTypeV v tv c ())]
πs, RTypeV v tv c r
t') = RTypeV v tv c r
-> ([(RTVUV v tv c, r)], [PVarV v (RTypeV v tv c ())],
    RTypeV v tv c r)
forall v tv c r.
RTypeV v tv c r
-> ([(RTVar c (RTypeV v tv c ()), r)],
    [PVarV v (RTypeV v tv c ())], RTypeV v tv c r)
bkUniv RTypeV v tv c r
t in ([(RTVUV v tv c, r)]
αs, PVarV v (RTypeV v tv c ())
πPVarV v (RTypeV v tv c ())
-> [PVarV v (RTypeV v tv c ())] -> [PVarV v (RTypeV v tv c ())]
forall a. a -> [a] -> [a]
:[PVarV v (RTypeV v tv c ())]
πs, RTypeV v tv c r
t')
bkUniv RTypeV v tv c r
t             = ([], [], RTypeV 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 v tv c r.
RTypeV v tv c r
-> ([(RTVar c (RTypeV v tv c ()), r)],
    [PVarV v (RTypeV v tv c ())], RTypeV 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 :: RTypeV Symbol t t1 a
t@(RApp t
c [RTypeV Symbol t t1 a]
_ [RTPropV Symbol t t1 a]
_ a
_) RTypeV Symbol t t1 a
t' a
r)
  | t -> Bool
forall c. TyConable c => c -> Bool
isClass t
c
  = let ([Symbol]
xs, [RTypeV Symbol t t1 a]
ts, [a]
rs, RTypeV Symbol t t1 a
t'') = RTypeV Symbol t t1 a
-> ([Symbol], [RTypeV Symbol t t1 a], [a], RTypeV 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' RTypeV Symbol t t1 a
t' in (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
xs, RTypeV Symbol t t1 a
tRTypeV Symbol t t1 a
-> [RTypeV Symbol t t1 a] -> [RTypeV Symbol t t1 a]
forall a. a -> [a] -> [a]
:[RTypeV Symbol t t1 a]
ts, a
ra -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
rs, RTypeV Symbol t t1 a
t'')
bkClass' (RRTy [(Symbol, RTypeV Symbol t t1 a)]
e a
r Oblig
o RTypeV Symbol t t1 a
t)
  = let ([Symbol]
xs, [RTypeV Symbol t t1 a]
ts, [a]
rs, RTypeV Symbol t t1 a
t'') = RTypeV Symbol t t1 a
-> ([Symbol], [RTypeV Symbol t t1 a], [a], RTypeV 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' RTypeV Symbol t t1 a
t in ([Symbol]
xs, [RTypeV Symbol t t1 a]
ts, [a]
rs, [(Symbol, RTypeV Symbol t t1 a)]
-> a -> Oblig -> RTypeV Symbol t t1 a -> RTypeV Symbol t t1 a
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy [(Symbol, RTypeV Symbol t t1 a)]
e a
r Oblig
o RTypeV Symbol t t1 a
t'')
bkClass' RTypeV Symbol t t1 a
t
  = ([], [],[],RTypeV Symbol t t1 a
t)

bkClass :: (F.PPrint c, TyConable c) => RType c tv r -> ([(c, [RType c tv r])], RType c tv r)
bkClass :: forall c tv r.
(PPrint c, TyConable c) =>
RType c tv r -> ([(c, [RType c tv r])], RType c tv r)
bkClass (RFun Symbol
_ RFInfo
_ (RApp c
c [RTypeV Symbol c tv r]
t [RTPropV Symbol c tv r]
_ r
_) RTypeV Symbol 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, [RTypeV Symbol c tv r])]
cs, RTypeV Symbol c tv r
t'') = RTypeV Symbol c tv r
-> ([(c, [RTypeV Symbol c tv r])], RTypeV Symbol c tv r)
forall c tv r.
(PPrint c, TyConable c) =>
RType c tv r -> ([(c, [RType c tv r])], RType c tv r)
bkClass RTypeV Symbol c tv r
t' in ((c
c, [RTypeV Symbol c tv r]
t)(c, [RTypeV Symbol c tv r])
-> [(c, [RTypeV Symbol c tv r])] -> [(c, [RTypeV Symbol c tv r])]
forall a. a -> [a] -> [a]
:[(c, [RTypeV Symbol c tv r])]
cs, RTypeV Symbol c tv r
t'')
bkClass (RRTy [(Symbol, RTypeV Symbol c tv r)]
e r
r Oblig
o RTypeV Symbol c tv r
t)
  = let ([(c, [RTypeV Symbol c tv r])]
cs, RTypeV Symbol c tv r
t') = RTypeV Symbol c tv r
-> ([(c, [RTypeV Symbol c tv r])], RTypeV Symbol c tv r)
forall c tv r.
(PPrint c, TyConable c) =>
RType c tv r -> ([(c, [RType c tv r])], RType c tv r)
bkClass RTypeV Symbol c tv r
t in ([(c, [RTypeV Symbol c tv r])]
cs, [(Symbol, RTypeV Symbol c tv r)]
-> r -> Oblig -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy [(Symbol, RTypeV Symbol c tv r)]
e r
r Oblig
o RTypeV Symbol c tv r
t')
bkClass RTypeV Symbol c tv r
t
  = ([], RTypeV Symbol c tv r
t)

rFun :: Monoid r => Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
rFun :: forall r v c tv.
Monoid r =>
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
rFun Symbol
b RTypeV v c tv r
t RTypeV v c tv r
t' = Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
b RFInfo
defRFInfo RTypeV v c tv r
t RTypeV v c tv r
t' r
forall a. Monoid a => a
mempty

rFun' :: Monoid r => RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun' :: forall r c tv.
Monoid 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 v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
b RFInfo
i RType c tv r
t RType c tv r
t' r
forall a. Monoid a => a
mempty

rFunDebug :: Monoid r => Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFunDebug :: forall r c tv.
Monoid 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 v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
b (Bool -> RFInfo
classRFInfo Bool
True) RType c tv r
t RType c tv r
t' r
forall a. Monoid a => a
mempty

rCls :: Monoid r => Ghc.TyCon -> [RType RTyCon tv r] -> RType RTyCon tv r
rCls :: forall r tv.
Monoid r =>
TyCon -> [RType RTyCon tv r] -> RType RTyCon tv r
rCls TyCon
c [RType RTyCon tv r]
ts   = RTyCon
-> [RType RTyCon tv r]
-> [RTPropV Symbol RTyCon tv r]
-> r
-> RType RTyCon tv r
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp (TyCon -> [PVar RSort] -> TyConInfo -> RTyCon
RTyCon TyCon
c [] TyConInfo
defaultTyConInfo) [RType RTyCon tv r]
ts [] r
forall a. Monoid a => a
mempty

rRCls :: Monoid r => c -> [RType c tv r] -> RType c tv r
rRCls :: forall r c tv. Monoid r => c -> [RType c tv r] -> RType c tv r
rRCls c
rc [RType c tv r]
ts = c -> [RType c tv r] -> [RTPropV Symbol c tv r] -> r -> RType c tv r
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp c
rc [RType c tv r]
ts [] r
forall a. Monoid a => a
mempty

addInvCond :: SpecType -> RReft -> SpecType
addInvCond :: SpecType -> RReft -> SpecType
addInvCond SpecType
t RReft
r'
  | ReftV Symbol -> Bool
forall r. Reftable r => r -> Bool
isTauto (ReftV Symbol -> Bool) -> ReftV Symbol -> Bool
forall a b. (a -> b) -> a -> b
$ RReft -> ReftV Symbol
forall v r. UReftV v r -> r
ur_reft RReft
r' -- null rv
  = SpecType
t
  | Bool
otherwise
  = RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
fromRTypeRep (RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType)
-> RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ RTypeRepV Symbol RTyCon RTyVar RReft
trep {ty_res = RRTy [(x', tbd)] r OInv tbd}
  where
    trep :: RTypeRepV Symbol RTyCon RTyVar RReft
trep = SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep SpecType
t
    tbd :: SpecType
tbd  = RTypeRepV Symbol RTyCon RTyVar RReft -> SpecType
forall v c tv r. RTypeRepV v c tv r -> RTypeV v c tv r
ty_res RTypeRepV Symbol RTyCon RTyVar RReft
trep
    r :: RReft
r    = RReft
r' {ur_reft = F.Reft (v, rx)}
    su :: (Symbol, ExprV Symbol)
su   = (Symbol
v, Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar Symbol
x')
    x' :: Symbol
x'   = Symbol
"xInv"
    rx :: ExprV Symbol
rx   = ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
F.PIff (Symbol -> ExprV Symbol
forall v. v -> ExprV v
F.EVar Symbol
v) (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ ExprV Symbol -> (Symbol, ExprV Symbol) -> ExprV Symbol
forall a. Subable a => a -> (Symbol, ExprV Symbol) -> a
F.subst1 ExprV Symbol
rv (Symbol, ExprV Symbol)
su
    F.Reft(Symbol
v, ExprV Symbol
rv) = RReft -> ReftV Symbol
forall v r. UReftV v r -> r
ur_reft RReft
r'


instance (Reftable r, TyConable c) => F.Subable (RTProp c tv r) where
  syms :: RTProp c tv r -> [Symbol]
syms (RProp  [(Symbol, RTypeV Symbol c tv ())]
ss RTypeV Symbol c tv r
r)     = ((Symbol, RTypeV Symbol c tv ()) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, RTypeV Symbol c tv ()) -> Symbol)
-> [(Symbol, RTypeV Symbol c tv ())] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RTypeV Symbol c tv ())]
ss) [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RTypeV Symbol c tv r -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms RTypeV Symbol c tv r
r

  subst :: Subst -> RTProp c tv r -> RTProp c tv r
subst Subst
su (RProp [(Symbol, RTypeV Symbol c tv ())]
ss (RHole r
r)) = [(Symbol, RTypeV Symbol c tv ())]
-> RTypeV Symbol c tv r -> RTProp c tv r
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RTypeV Symbol c tv ())]
ss (r -> RTypeV Symbol c tv r
forall v c tv r. r -> RTypeV v c tv r
RHole (Subst -> r -> r
forall a. Subable a => Subst -> a -> a
F.subst Subst
su r
r))
  subst Subst
su (RProp  [(Symbol, RTypeV Symbol c tv ())]
ss RTypeV Symbol c tv r
t) = [(Symbol, RTypeV Symbol c tv ())]
-> RTypeV Symbol c tv r -> RTProp c tv r
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RTypeV Symbol c tv ())]
ss (Subst -> r -> r
forall a. Subable a => Subst -> a -> a
F.subst Subst
su (r -> r) -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTypeV Symbol c tv r
t)

  substf :: (Symbol -> ExprV Symbol) -> RTProp c tv r -> RTProp c tv r
substf Symbol -> ExprV Symbol
f (RProp [(Symbol, RTypeV Symbol c tv ())]
ss (RHole r
r)) = [(Symbol, RTypeV Symbol c tv ())]
-> RTypeV Symbol c tv r -> RTProp c tv r
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RTypeV Symbol c tv ())]
ss (r -> RTypeV Symbol c tv r
forall v c tv r. r -> RTypeV v c tv r
RHole ((Symbol -> ExprV Symbol) -> r -> r
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
F.substf Symbol -> ExprV Symbol
f r
r))
  substf Symbol -> ExprV Symbol
f (RProp  [(Symbol, RTypeV Symbol c tv ())]
ss RTypeV Symbol c tv r
t) = [(Symbol, RTypeV Symbol c tv ())]
-> RTypeV Symbol c tv r -> RTProp c tv r
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RTypeV Symbol c tv ())]
ss ((Symbol -> ExprV Symbol) -> r -> r
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
F.substf Symbol -> ExprV Symbol
f (r -> r) -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTypeV Symbol c tv r
t)

  substa :: (Symbol -> Symbol) -> RTProp c tv r -> RTProp c tv r
substa Symbol -> Symbol
f (RProp [(Symbol, RTypeV Symbol c tv ())]
ss (RHole r
r)) = [(Symbol, RTypeV Symbol c tv ())]
-> RTypeV Symbol c tv r -> RTProp c tv r
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RTypeV Symbol c tv ())]
ss (r -> RTypeV Symbol c tv r
forall v c tv r. r -> RTypeV v c tv r
RHole ((Symbol -> Symbol) -> r -> r
forall a. Subable a => (Symbol -> Symbol) -> a -> a
F.substa Symbol -> Symbol
f r
r))
  substa Symbol -> Symbol
f (RProp  [(Symbol, RTypeV Symbol c tv ())]
ss RTypeV Symbol c tv r
t) = [(Symbol, RTypeV Symbol c tv ())]
-> RTypeV Symbol c tv r -> RTProp c tv r
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RTypeV Symbol c tv ())]
ss ((Symbol -> Symbol) -> r -> r
forall a. Subable a => (Symbol -> Symbol) -> a -> a
F.substa Symbol -> Symbol
f (r -> r) -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTypeV Symbol c tv r
t)


instance (F.Subable r, Reftable r, TyConable c) => F.Subable (RType c tv r) where
  syms :: RType c tv r -> [Symbol]
syms        = Bool
-> (SEnv (RType c tv r) -> r -> [Symbol] -> [Symbol])
-> [Symbol]
-> RType c tv r
-> [Symbol]
forall r c tv a.
(Reftable r, TyConable c) =>
Bool
-> (SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a
foldReft Bool
False (\SEnv (RType c tv r)
_ r
r [Symbol]
acc -> r -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms r
r [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
acc) []
  -- 'substa' will substitute bound vars
  substa :: (Symbol -> Symbol) -> RType c tv r -> RType c tv r
substa Symbol -> Symbol
f    = ([Symbol] -> ExprV Symbol -> ExprV Symbol)
-> [Symbol] -> RType c tv r -> RType c tv r
forall c tv r.
([Symbol] -> ExprV Symbol -> ExprV Symbol)
-> [Symbol] -> RType c tv r -> RType c tv r
emapExprArg (\[Symbol]
_ -> (Symbol -> Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> Symbol) -> a -> a
F.substa Symbol -> Symbol
f) []      (RType c tv r -> RType c tv r)
-> (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (r -> r) -> RType c tv r -> RType c tv r
forall r1 r2 v c tv.
(r1 -> r2) -> RTypeV v c tv r1 -> RTypeV v c tv r2
mapReft  ((Symbol -> Symbol) -> r -> r
forall a. Subable a => (Symbol -> Symbol) -> a -> a
F.substa Symbol -> Symbol
f)
  -- 'substf' will NOT substitute bound vars
  substf :: (Symbol -> ExprV Symbol) -> RType c tv r -> RType c tv r
substf Symbol -> ExprV Symbol
f    = ([Symbol] -> ExprV Symbol -> ExprV Symbol)
-> [Symbol] -> RType c tv r -> RType c tv r
forall c tv r.
([Symbol] -> ExprV Symbol -> ExprV Symbol)
-> [Symbol] -> RType c tv r -> RType c tv r
emapExprArg (\[Symbol]
_ -> (Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
F.substf Symbol -> ExprV Symbol
f) []      (RType c tv r -> RType c tv r)
-> (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Symbol] -> r -> r) -> [Symbol] -> RType c tv r -> RType c tv r
forall r1 r2 v c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
emapReft ((Symbol -> ExprV Symbol) -> r -> r
forall a. Subable a => (Symbol -> ExprV Symbol) -> a -> a
F.substf ((Symbol -> ExprV Symbol) -> r -> r)
-> ([Symbol] -> Symbol -> ExprV Symbol) -> [Symbol] -> r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> ExprV Symbol) -> [Symbol] -> Symbol -> ExprV Symbol
F.substfExcept Symbol -> ExprV Symbol
f) []
  subst :: Subst -> RType c tv r -> RType c tv r
subst Subst
su    = ([Symbol] -> ExprV Symbol -> ExprV Symbol)
-> [Symbol] -> RType c tv r -> RType c tv r
forall c tv r.
([Symbol] -> ExprV Symbol -> ExprV Symbol)
-> [Symbol] -> RType c tv r -> RType c tv r
emapExprArg (\[Symbol]
_ -> Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
F.subst Subst
su) []      (RType c tv r -> RType c tv r)
-> (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Symbol] -> r -> r) -> [Symbol] -> RType c tv r -> RType c tv r
forall r1 r2 v c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
emapReft (Subst -> r -> r
forall a. Subable a => Subst -> a -> a
F.subst  (Subst -> r -> r) -> ([Symbol] -> Subst) -> [Symbol] -> r -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> [Symbol] -> Subst
F.substExcept Subst
su) []
  subst1 :: RType c tv r -> (Symbol, ExprV Symbol) -> RType c tv r
subst1 RType c tv r
t (Symbol, ExprV Symbol)
su = ([Symbol] -> ExprV Symbol -> ExprV Symbol)
-> [Symbol] -> RType c tv r -> RType c tv r
forall c tv r.
([Symbol] -> ExprV Symbol -> ExprV Symbol)
-> [Symbol] -> RType c tv r -> RType c tv r
emapExprArg (\[Symbol]
_ ExprV Symbol
e -> ExprV Symbol -> (Symbol, ExprV Symbol) -> ExprV Symbol
forall a. Subable a => a -> (Symbol, ExprV Symbol) -> a
F.subst1 ExprV Symbol
e (Symbol, ExprV Symbol)
su) [] (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
forall a b. (a -> b) -> a -> b
$ ([Symbol] -> r -> r) -> [Symbol] -> RType c tv r -> RType c tv r
forall r1 r2 v c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
emapReft (\[Symbol]
xs r
r -> [Symbol] -> r -> (Symbol, ExprV Symbol) -> r
forall a. Subable a => [Symbol] -> a -> (Symbol, ExprV Symbol) -> a
F.subst1Except [Symbol]
xs r
r (Symbol, ExprV Symbol)
su) [] RType c tv r
t


--------------------------------------------------------------------------------
-- | Visitors ------------------------------------------------------------------
--------------------------------------------------------------------------------
mapExprReft :: (Symbol -> Expr -> Expr) -> RType c tv RReft -> RType c tv RReft
mapExprReft :: forall c tv.
(Symbol -> ExprV Symbol -> ExprV Symbol)
-> RType c tv RReft -> RType c tv RReft
mapExprReft Symbol -> ExprV Symbol -> ExprV Symbol
f = (RReft -> RReft)
-> RTypeV Symbol c tv RReft -> RTypeV Symbol c tv RReft
forall r1 r2 v c tv.
(r1 -> r2) -> RTypeV v c tv r1 -> RTypeV v c tv r2
mapReft RReft -> RReft
forall {v}. UReftV v (ReftV Symbol) -> UReftV v (ReftV Symbol)
g
  where
    g :: UReftV v (ReftV Symbol) -> UReftV v (ReftV Symbol)
g (MkUReft (F.Reft (Symbol
x, ExprV Symbol
e)) PredicateV v
p) = ReftV Symbol -> PredicateV v -> UReftV v (ReftV Symbol)
forall v r. r -> PredicateV v -> UReftV v r
MkUReft ((Symbol, ExprV Symbol) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
F.Reft (Symbol
x, Symbol -> ExprV Symbol -> ExprV Symbol
f Symbol
x ExprV Symbol
e)) PredicateV v
p

-- const False (not dropping dict) is probably fine since there will not be refinement on
-- dictionaries
isTrivial :: (Reftable r, TyConable c) => RType c tv r -> Bool
isTrivial :: forall r c tv. (Reftable r, TyConable c) => RType c tv r -> Bool
isTrivial = Bool
-> (SEnv (RType c tv r) -> r -> Bool -> Bool)
-> Bool
-> RType c tv r
-> Bool
forall r c tv a.
(Reftable r, TyConable c) =>
Bool
-> (SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a
foldReft Bool
False (\SEnv (RType c tv r)
_ r
r Bool
b -> r -> Bool
forall r. Reftable r => r -> Bool
isTauto r
r Bool -> Bool -> Bool
&& Bool
b) Bool
True

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

emapReft ::  ([Symbol] -> r1 -> r2) -> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
emapReft :: forall r1 r2 v c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ (RVar tv
α r1
r)        = tv -> r2 -> RTypeV v c tv r2
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar  tv
α ([Symbol] -> r1 -> r2
f [Symbol]
γ r1
r)
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ (RAllT RTVUV v c tv
α RTypeV v c tv r1
t r1
r)     = RTVUV v c tv -> RTypeV v c tv r2 -> r2 -> RTypeV v c tv r2
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV v c tv
α (([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
forall r1 r2 v c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ RTypeV v c tv r1
t) ([Symbol] -> r1 -> r2
f [Symbol]
γ r1
r)
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ (RAllP PVUV v c tv
π RTypeV v c tv r1
t)       = PVUV v c tv -> RTypeV v c tv r2 -> RTypeV v c tv r2
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV v c tv
π (([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
forall r1 r2 v c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ RTypeV v c tv r1
t)
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ (RFun Symbol
x RFInfo
i RTypeV v c tv r1
t RTypeV v c tv r1
t' r1
r) = Symbol
-> RFInfo
-> RTypeV v c tv r2
-> RTypeV v c tv r2
-> r2
-> RTypeV v c tv r2
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun  Symbol
x RFInfo
i (([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
forall r1 r2 v c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ RTypeV v c tv r1
t) (([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
forall r1 r2 v c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
emapReft [Symbol] -> r1 -> r2
f (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
γ) RTypeV v c tv r1
t') ([Symbol] -> r1 -> r2
f (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
γ) r1
r)
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ (RApp c
c [RTypeV v c tv r1]
ts [RTPropV v c tv r1]
rs r1
r)  = c
-> [RTypeV v c tv r2]
-> [RTPropV v c tv r2]
-> r2
-> RTypeV v c tv r2
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp  c
c (([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
forall r1 r2 v c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ (RTypeV v c tv r1 -> RTypeV v c tv r2)
-> [RTypeV v c tv r1] -> [RTypeV v c tv r2]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeV v c tv r1]
ts) (([Symbol] -> r1 -> r2)
-> [Symbol] -> RTPropV v c tv r1 -> RTPropV v c tv r2
forall t s v c tv.
([Symbol] -> t -> s)
-> [Symbol] -> RTPropV v c tv t -> RTPropV v c tv s
emapRef [Symbol] -> r1 -> r2
f [Symbol]
γ (RTPropV v c tv r1 -> RTPropV v c tv r2)
-> [RTPropV v c tv r1] -> [RTPropV v c tv r2]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropV v c tv r1]
rs) ([Symbol] -> r1 -> r2
f [Symbol]
γ r1
r)
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ (RAllE Symbol
z RTypeV v c tv r1
t RTypeV v c tv r1
t')    = Symbol -> RTypeV v c tv r2 -> RTypeV v c tv r2 -> RTypeV v c tv r2
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
RAllE Symbol
z (([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
forall r1 r2 v c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ RTypeV v c tv r1
t) (([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
forall r1 r2 v c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ RTypeV v c tv r1
t')
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ (REx Symbol
z RTypeV v c tv r1
t RTypeV v c tv r1
t')      = Symbol -> RTypeV v c tv r2 -> RTypeV v c tv r2 -> RTypeV v c tv r2
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
REx   Symbol
z (([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
forall r1 r2 v c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ RTypeV v c tv r1
t) (([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
forall r1 r2 v c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ RTypeV v c tv r1
t')
emapReft [Symbol] -> r1 -> r2
_ [Symbol]
_ (RExprArg Located (ExprV v)
e)      = Located (ExprV v) -> RTypeV v c tv r2
forall v c tv r. Located (ExprV v) -> RTypeV v c tv r
RExprArg Located (ExprV v)
e
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ (RAppTy RTypeV v c tv r1
t RTypeV v c tv r1
t' r1
r)   = RTypeV v c tv r2 -> RTypeV v c tv r2 -> r2 -> RTypeV v c tv r2
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy (([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
forall r1 r2 v c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ RTypeV v c tv r1
t) (([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
forall r1 r2 v c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ RTypeV v c tv r1
t') ([Symbol] -> r1 -> r2
f [Symbol]
γ r1
r)
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ (RRTy [(Symbol, RTypeV v c tv r1)]
e r1
r Oblig
o RTypeV v c tv r1
t)    = [(Symbol, RTypeV v c tv r2)]
-> r2 -> Oblig -> RTypeV v c tv r2 -> RTypeV v c tv r2
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy  ((RTypeV v c tv r1 -> RTypeV v c tv r2)
-> (Symbol, RTypeV v c tv r1) -> (Symbol, RTypeV v c tv r2)
forall a b. (a -> b) -> (Symbol, a) -> (Symbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
forall r1 r2 v c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ) ((Symbol, RTypeV v c tv r1) -> (Symbol, RTypeV v c tv r2))
-> [(Symbol, RTypeV v c tv r1)] -> [(Symbol, RTypeV v c tv r2)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RTypeV v c tv r1)]
e) ([Symbol] -> r1 -> r2
f [Symbol]
γ r1
r) Oblig
o (([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
forall r1 r2 v c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ RTypeV v c tv r1
t)
emapReft [Symbol] -> r1 -> r2
f [Symbol]
γ (RHole r1
r)         = r2 -> RTypeV v c tv r2
forall v c tv r. r -> RTypeV v c tv r
RHole ([Symbol] -> r1 -> r2
f [Symbol]
γ r1
r)

emapRef :: ([Symbol] -> t -> s) ->  [Symbol] -> RTPropV v c tv t -> RTPropV v c tv s
emapRef :: forall t s v c tv.
([Symbol] -> t -> s)
-> [Symbol] -> RTPropV v c tv t -> RTPropV v c tv s
emapRef  [Symbol] -> t -> s
f [Symbol]
γ (RProp [(Symbol, RTypeV v c tv ())]
s (RHole t
r))  = [(Symbol, RTypeV v c tv ())]
-> RTypeV v c tv s -> Ref (RTypeV v c tv ()) (RTypeV v c tv s)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RTypeV v c tv ())]
s (RTypeV v c tv s -> Ref (RTypeV v c tv ()) (RTypeV v c tv s))
-> RTypeV v c tv s -> Ref (RTypeV v c tv ()) (RTypeV v c tv s)
forall a b. (a -> b) -> a -> b
$ s -> RTypeV v c tv s
forall v c tv r. r -> RTypeV v c tv r
RHole ([Symbol] -> t -> s
f [Symbol]
γ t
r)
emapRef  [Symbol] -> t -> s
f [Symbol]
γ (RProp [(Symbol, RTypeV v c tv ())]
s RTypeV v c tv t
t)         = [(Symbol, RTypeV v c tv ())]
-> RTypeV v c tv s -> Ref (RTypeV v c tv ()) (RTypeV v c tv s)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RTypeV v c tv ())]
s (RTypeV v c tv s -> Ref (RTypeV v c tv ()) (RTypeV v c tv s))
-> RTypeV v c tv s -> Ref (RTypeV v c tv ()) (RTypeV v c tv s)
forall a b. (a -> b) -> a -> b
$ ([Symbol] -> t -> s)
-> [Symbol] -> RTypeV v c tv t -> RTypeV v c tv s
forall r1 r2 v c tv.
([Symbol] -> r1 -> r2)
-> [Symbol] -> RTypeV v c tv r1 -> RTypeV v c tv r2
emapReft [Symbol] -> t -> s
f [Symbol]
γ RTypeV v c tv t
t

mapRTypeV ::  (v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV :: forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV v -> v'
_ (RVar tv
α r
r)        = tv -> r -> RTypeV v' c tv r
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar tv
α r
r
mapRTypeV v -> v'
f (RAllT RTVUV v c tv
α RTypeV v c tv r
t r
r)     = RTVUV v' c tv -> RTypeV v' c tv r -> r -> RTypeV v' c tv r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT ((RTypeV v c tv () -> RTypeV v' c tv ())
-> RTVUV v c tv -> RTVUV 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') -> RTypeV v c tv () -> RTypeV v' c tv ()
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV v -> v'
f) RTVUV v c tv
α) ((v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV v -> v'
f RTypeV v c tv r
t) r
r
mapRTypeV v -> v'
f (RAllP PVUV v c tv
π RTypeV v c tv r
t)       = PVUV v' c tv -> RTypeV v' c tv r -> RTypeV v' c tv r
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP ((v -> v')
-> (RTypeV v c tv () -> RTypeV v' c tv ())
-> PVUV v c tv
-> PVUV v' c tv
forall v v' t t'.
(v -> v') -> (t -> t') -> PVarV v t -> PVarV v' t'
mapPVarV v -> v'
f ((v -> v') -> RTypeV v c tv () -> RTypeV v' c tv ()
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV v -> v'
f) PVUV v c tv
π) ((v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV v -> v'
f RTypeV v c tv r
t)
mapRTypeV v -> v'
f (RFun Symbol
x RFInfo
i RTypeV v c tv r
t RTypeV v c tv r
t' r
r) = Symbol
-> RFInfo
-> RTypeV v' c tv r
-> RTypeV v' c tv r
-> r
-> RTypeV v' c tv r
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
x RFInfo
i ((v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV v -> v'
f RTypeV v c tv r
t) ((v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV v -> v'
f RTypeV v c tv r
t') r
r
mapRTypeV v -> v'
f (RApp c
c [RTypeV v c tv r]
ts [RTPropV v c tv r]
rs r
r)  = c
-> [RTypeV v' c tv r]
-> [RTPropV v' c tv r]
-> r
-> RTypeV v' c tv r
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp c
c ((v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV v -> v'
f (RTypeV v c tv r -> RTypeV v' c tv r)
-> [RTypeV v c tv r] -> [RTypeV v' c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeV v c tv r]
ts) (RTPropV v c tv r -> RTPropV v' c tv r
forall {c} {tv} {r} {c} {tv} {r}.
Ref (RTypeV v c tv r) (RTypeV v c tv r)
-> Ref (RTypeV v' c tv r) (RTypeV v' c tv r)
mapRefV (RTPropV v c tv r -> RTPropV v' c tv r)
-> [RTPropV v c tv r] -> [RTPropV v' c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropV v c tv r]
rs) r
r
  where
    mapRefV :: Ref (RTypeV v c tv r) (RTypeV v c tv r)
-> Ref (RTypeV v' c tv r) (RTypeV v' c tv r)
mapRefV (RProp [(Symbol, RTypeV v c tv r)]
ss RTypeV v c tv r
t) = [(Symbol, RTypeV v' c tv r)]
-> RTypeV v' c tv r -> Ref (RTypeV v' c tv r) (RTypeV v' c tv r)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp (((Symbol, RTypeV v c tv r) -> (Symbol, RTypeV v' c tv r))
-> [(Symbol, RTypeV v c tv r)] -> [(Symbol, RTypeV v' c tv r)]
forall a b. (a -> b) -> [a] -> [b]
map ((RTypeV v c tv r -> RTypeV v' c tv r)
-> (Symbol, RTypeV v c tv r) -> (Symbol, RTypeV v' 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 ((v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV v -> v'
f)) [(Symbol, RTypeV v c tv r)]
ss) ((v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV v -> v'
f RTypeV v c tv r
t)
mapRTypeV v -> v'
f (RAllE Symbol
z RTypeV v c tv r
t RTypeV v c tv r
t')    = Symbol -> RTypeV v' c tv r -> RTypeV v' c tv r -> RTypeV v' c tv r
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
RAllE Symbol
z ((v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV v -> v'
f RTypeV v c tv r
t) ((v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV v -> v'
f RTypeV v c tv r
t')
mapRTypeV v -> v'
f (REx Symbol
z RTypeV v c tv r
t RTypeV v c tv r
t')      = Symbol -> RTypeV v' c tv r -> RTypeV v' c tv r -> RTypeV v' c tv r
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
REx Symbol
z ((v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV v -> v'
f RTypeV v c tv r
t) ((v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV v -> v'
f RTypeV v c tv r
t')
mapRTypeV v -> v'
f (RExprArg Located (ExprV v)
e)      = Located (ExprV v') -> RTypeV v' c tv r
forall v c tv r. Located (ExprV v) -> RTypeV v c tv r
RExprArg ((ExprV v -> ExprV v') -> Located (ExprV v) -> Located (ExprV 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') -> ExprV v -> ExprV v'
forall a b. (a -> b) -> ExprV a -> ExprV b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap v -> v'
f) Located (ExprV v)
e)
mapRTypeV v -> v'
f (RAppTy RTypeV v c tv r
t RTypeV v c tv r
t' r
r)   = RTypeV v' c tv r -> RTypeV v' c tv r -> r -> RTypeV v' c tv r
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy ((v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV v -> v'
f RTypeV v c tv r
t) ((v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV v -> v'
f RTypeV v c tv r
t') r
r
mapRTypeV v -> v'
f (RRTy [(Symbol, RTypeV v c tv r)]
e r
r Oblig
o RTypeV v c tv r
t)    = [(Symbol, RTypeV v' c tv r)]
-> r -> Oblig -> RTypeV v' c tv r -> RTypeV v' c tv r
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy ((RTypeV v c tv r -> RTypeV v' c tv r)
-> (Symbol, RTypeV v c tv r) -> (Symbol, RTypeV v' 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 ((v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV v -> v'
f) ((Symbol, RTypeV v c tv r) -> (Symbol, RTypeV v' c tv r))
-> [(Symbol, RTypeV v c tv r)] -> [(Symbol, RTypeV v' c tv r)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RTypeV v c tv r)]
e) r
r Oblig
o ((v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV v -> v'
f RTypeV v c tv r
t)
mapRTypeV v -> v'
_ (RHole r
r)         = r -> RTypeV v' c tv r
forall v c tv r. r -> RTypeV v c tv r
RHole r
r

mapRTypeVM :: Monad m => (v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
mapRTypeVM :: forall (m :: * -> *) v v' c tv r.
Monad m =>
(v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
mapRTypeVM v -> m v'
_ (RVar tv
α r
r)        = RTypeV v' c tv r -> m (RTypeV v' c tv r)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (RTypeV v' c tv r -> m (RTypeV v' c tv r))
-> RTypeV v' c tv r -> m (RTypeV v' c tv r)
forall a b. (a -> b) -> a -> b
$ tv -> r -> RTypeV v' c tv r
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar tv
α r
r
mapRTypeVM v -> m v'
f (RAllT RTVUV v c tv
α RTypeV v c tv r
t r
r)     = RTVUV v' c tv -> RTypeV v' c tv r -> r -> RTypeV v' c tv r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT (RTVUV v' c tv -> RTypeV v' c tv r -> r -> RTypeV v' c tv r)
-> m (RTVUV v' c tv)
-> m (RTypeV v' c tv r -> r -> RTypeV v' c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RTypeV v c tv () -> m (RTypeV v' c tv ()))
-> RTVUV v c tv -> m (RTVUV 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') -> RTypeV v c tv () -> m (RTypeV v' c tv ())
forall (m :: * -> *) v v' c tv r.
Monad m =>
(v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
mapRTypeVM v -> m v'
f) RTVUV v c tv
α m (RTypeV v' c tv r -> r -> RTypeV v' c tv r)
-> m (RTypeV v' c tv r) -> m (r -> RTypeV 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') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
forall (m :: * -> *) v v' c tv r.
Monad m =>
(v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
mapRTypeVM v -> m v'
f RTypeV v c tv r
t m (r -> RTypeV v' c tv r) -> m r -> m (RTypeV 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 PVUV v c tv
π RTypeV v c tv r
t)       = PVUV v' c tv -> RTypeV v' c tv r -> RTypeV v' c tv r
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP (PVUV v' c tv -> RTypeV v' c tv r -> RTypeV v' c tv r)
-> m (PVUV v' c tv) -> m (RTypeV v' c tv r -> RTypeV v' c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Symbol] -> v -> m v')
-> ([Symbol] -> RTypeV v c tv () -> m (RTypeV v' c tv ()))
-> PVUV v c tv
-> m (PVUV v' c tv)
forall (m :: * -> *) v v' t t'.
Monad m =>
([Symbol] -> v -> m v')
-> ([Symbol] -> t -> m t') -> PVarV v t -> m (PVarV v' t')
emapPVarVM ((v -> m v') -> [Symbol] -> v -> m v'
forall a b. a -> b -> a
const v -> m v'
f) ((RTypeV v c tv () -> m (RTypeV v' c tv ()))
-> [Symbol] -> RTypeV v c tv () -> m (RTypeV v' c tv ())
forall a b. a -> b -> a
const ((v -> m v') -> RTypeV v c tv () -> m (RTypeV v' c tv ())
forall (m :: * -> *) v v' c tv r.
Monad m =>
(v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
mapRTypeVM v -> m v'
f)) PVUV v c tv
π m (RTypeV v' c tv r -> RTypeV v' c tv r)
-> m (RTypeV v' c tv r) -> m (RTypeV 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') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
forall (m :: * -> *) v v' c tv r.
Monad m =>
(v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
mapRTypeVM v -> m v'
f RTypeV v c tv r
t
mapRTypeVM v -> m v'
f (RFun Symbol
x RFInfo
i RTypeV v c tv r
t RTypeV v c tv r
t' r
r) = Symbol
-> RFInfo
-> RTypeV v' c tv r
-> RTypeV v' c tv r
-> r
-> RTypeV v' c tv r
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
x RFInfo
i (RTypeV v' c tv r -> RTypeV v' c tv r -> r -> RTypeV v' c tv r)
-> m (RTypeV v' c tv r)
-> m (RTypeV v' c tv r -> r -> RTypeV v' c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
forall (m :: * -> *) v v' c tv r.
Monad m =>
(v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
mapRTypeVM v -> m v'
f RTypeV v c tv r
t m (RTypeV v' c tv r -> r -> RTypeV v' c tv r)
-> m (RTypeV v' c tv r) -> m (r -> RTypeV 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') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
forall (m :: * -> *) v v' c tv r.
Monad m =>
(v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
mapRTypeVM v -> m v'
f RTypeV v c tv r
t' m (r -> RTypeV v' c tv r) -> m r -> m (RTypeV 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 [RTypeV v c tv r]
ts [RTPropV v c tv r]
rs r
r)  = c
-> [RTypeV v' c tv r]
-> [RTPropV v' c tv r]
-> r
-> RTypeV v' c tv r
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp c
c ([RTypeV v' c tv r]
 -> [RTPropV v' c tv r] -> r -> RTypeV v' c tv r)
-> m [RTypeV v' c tv r]
-> m ([RTPropV v' c tv r] -> r -> RTypeV v' c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RTypeV v c tv r -> m (RTypeV v' c tv r))
-> [RTypeV v c tv r] -> m [RTypeV 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') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
forall (m :: * -> *) v v' c tv r.
Monad m =>
(v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
mapRTypeVM v -> m v'
f) [RTypeV v c tv r]
ts m ([RTPropV v' c tv r] -> r -> RTypeV v' c tv r)
-> m [RTPropV v' c tv r] -> m (r -> RTypeV 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
<*> (RTPropV v c tv r -> m (RTPropV v' c tv r))
-> [RTPropV v c tv r] -> m [RTPropV 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 RTPropV v c tv r -> m (RTPropV v' c tv r)
forall {c} {tv} {r} {c} {tv} {r}.
Ref (RTypeV v c tv r) (RTypeV v c tv r)
-> m (Ref (RTypeV v' c tv r) (RTypeV v' c tv r))
mapRefVM [RTPropV v c tv r]
rs m (r -> RTypeV v' c tv r) -> m r -> m (RTypeV 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 :: Ref (RTypeV v c tv r) (RTypeV v c tv r)
-> m (Ref (RTypeV v' c tv r) (RTypeV v' c tv r))
mapRefVM (RProp [(Symbol, RTypeV v c tv r)]
ss RTypeV v c tv r
t) = [(Symbol, RTypeV v' c tv r)]
-> RTypeV v' c tv r -> Ref (RTypeV v' c tv r) (RTypeV v' c tv r)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp ([(Symbol, RTypeV v' c tv r)]
 -> RTypeV v' c tv r -> Ref (RTypeV v' c tv r) (RTypeV v' c tv r))
-> m [(Symbol, RTypeV v' c tv r)]
-> m (RTypeV v' c tv r
      -> Ref (RTypeV v' c tv r) (RTypeV v' c tv r))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Symbol, RTypeV v c tv r) -> m (Symbol, RTypeV v' c tv r))
-> [(Symbol, RTypeV v c tv r)] -> m [(Symbol, RTypeV 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 ((RTypeV v c tv r -> m (RTypeV v' c tv r))
-> (Symbol, RTypeV v c tv r) -> m (Symbol, RTypeV 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) -> (Symbol, a) -> f (Symbol, b)
traverse ((v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
forall (m :: * -> *) v v' c tv r.
Monad m =>
(v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
mapRTypeVM v -> m v'
f)) [(Symbol, RTypeV v c tv r)]
ss m (RTypeV v' c tv r -> Ref (RTypeV v' c tv r) (RTypeV v' c tv r))
-> m (RTypeV v' c tv r)
-> m (Ref (RTypeV v' c tv r) (RTypeV 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') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
forall (m :: * -> *) v v' c tv r.
Monad m =>
(v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
mapRTypeVM v -> m v'
f RTypeV v c tv r
t
mapRTypeVM v -> m v'
f (RAllE Symbol
z RTypeV v c tv r
t RTypeV v c tv r
t')    = Symbol -> RTypeV v' c tv r -> RTypeV v' c tv r -> RTypeV v' c tv r
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
RAllE Symbol
z (RTypeV v' c tv r -> RTypeV v' c tv r -> RTypeV v' c tv r)
-> m (RTypeV v' c tv r) -> m (RTypeV v' c tv r -> RTypeV v' c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
forall (m :: * -> *) v v' c tv r.
Monad m =>
(v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
mapRTypeVM v -> m v'
f RTypeV v c tv r
t m (RTypeV v' c tv r -> RTypeV v' c tv r)
-> m (RTypeV v' c tv r) -> m (RTypeV 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') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
forall (m :: * -> *) v v' c tv r.
Monad m =>
(v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
mapRTypeVM v -> m v'
f RTypeV v c tv r
t'
mapRTypeVM v -> m v'
f (REx Symbol
z RTypeV v c tv r
t RTypeV v c tv r
t')      = Symbol -> RTypeV v' c tv r -> RTypeV v' c tv r -> RTypeV v' c tv r
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
REx Symbol
z (RTypeV v' c tv r -> RTypeV v' c tv r -> RTypeV v' c tv r)
-> m (RTypeV v' c tv r) -> m (RTypeV v' c tv r -> RTypeV v' c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
forall (m :: * -> *) v v' c tv r.
Monad m =>
(v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
mapRTypeVM v -> m v'
f RTypeV v c tv r
t m (RTypeV v' c tv r -> RTypeV v' c tv r)
-> m (RTypeV v' c tv r) -> m (RTypeV 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') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
forall (m :: * -> *) v v' c tv r.
Monad m =>
(v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
mapRTypeVM v -> m v'
f RTypeV v c tv r
t'
mapRTypeVM v -> m v'
f (RExprArg Located (ExprV v)
e)      = Located (ExprV v') -> RTypeV v' c tv r
forall v c tv r. Located (ExprV v) -> RTypeV v c tv r
RExprArg (Located (ExprV v') -> RTypeV v' c tv r)
-> m (Located (ExprV v')) -> m (RTypeV v' c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ExprV v -> m (ExprV v'))
-> Located (ExprV v) -> m (Located (ExprV 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') -> ExprV v -> m (ExprV 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) -> ExprV a -> f (ExprV b)
traverse v -> m v'
f) Located (ExprV v)
e
mapRTypeVM v -> m v'
f (RAppTy RTypeV v c tv r
t RTypeV v c tv r
t' r
r)   = RTypeV v' c tv r -> RTypeV v' c tv r -> r -> RTypeV v' c tv r
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy (RTypeV v' c tv r -> RTypeV v' c tv r -> r -> RTypeV v' c tv r)
-> m (RTypeV v' c tv r)
-> m (RTypeV v' c tv r -> r -> RTypeV v' c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
forall (m :: * -> *) v v' c tv r.
Monad m =>
(v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
mapRTypeVM v -> m v'
f RTypeV v c tv r
t m (RTypeV v' c tv r -> r -> RTypeV v' c tv r)
-> m (RTypeV v' c tv r) -> m (r -> RTypeV 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') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
forall (m :: * -> *) v v' c tv r.
Monad m =>
(v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
mapRTypeVM v -> m v'
f RTypeV v c tv r
t' m (r -> RTypeV v' c tv r) -> m r -> m (RTypeV 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 [(Symbol, RTypeV v c tv r)]
e r
r Oblig
o RTypeV v c tv r
t)    = [(Symbol, RTypeV v' c tv r)]
-> r -> Oblig -> RTypeV v' c tv r -> RTypeV v' c tv r
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy ([(Symbol, RTypeV v' c tv r)]
 -> r -> Oblig -> RTypeV v' c tv r -> RTypeV v' c tv r)
-> m [(Symbol, RTypeV v' c tv r)]
-> m (r -> Oblig -> RTypeV v' c tv r -> RTypeV v' c tv r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Symbol, RTypeV v c tv r) -> m (Symbol, RTypeV v' c tv r))
-> [(Symbol, RTypeV v c tv r)] -> m [(Symbol, RTypeV 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 ((RTypeV v c tv r -> m (RTypeV v' c tv r))
-> (Symbol, RTypeV v c tv r) -> m (Symbol, RTypeV 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) -> (Symbol, a) -> f (Symbol, b)
traverse ((v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
forall (m :: * -> *) v v' c tv r.
Monad m =>
(v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
mapRTypeVM v -> m v'
f)) [(Symbol, RTypeV v c tv r)]
e m (r -> Oblig -> RTypeV v' c tv r -> RTypeV v' c tv r)
-> m r -> m (Oblig -> RTypeV v' c tv r -> RTypeV 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 -> RTypeV v' c tv r -> RTypeV v' c tv r)
-> m Oblig -> m (RTypeV v' c tv r -> RTypeV 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 (RTypeV v' c tv r -> RTypeV v' c tv r)
-> m (RTypeV v' c tv r) -> m (RTypeV 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') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
forall (m :: * -> *) v v' c tv r.
Monad m =>
(v -> m v') -> RTypeV v c tv r -> m (RTypeV v' c tv r)
mapRTypeVM v -> m v'
f RTypeV v c tv r
t
mapRTypeVM v -> m v'
_ (RHole r
r)         = RTypeV v' c tv r -> m (RTypeV v' c tv r)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (r -> RTypeV v' c tv r
forall v c tv r. r -> RTypeV 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, ExprV 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') -> ExprV v -> m (ExprV v')
forall (m :: * -> *) v v'.
Monad m =>
([Symbol] -> v -> m v') -> ExprV v -> m (ExprV 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]
:)) ExprV v
e

-- The first parameter corresponds to the bscope config setting
emapReftM
  :: (Monad m, ToReftV r1, F.Symbolic tv)
  => Bool
  -> ([Symbol] -> v1 -> m v2)
  -> ([Symbol] -> r1 -> m r2)
  -> [Symbol]
  -> RTypeV v1 c tv r1
  -> m (RTypeV v2 c tv r2)
emapReftM :: forall (m :: * -> *) r1 tv v1 v2 r2 c.
(Monad m, ToReftV r1, Symbolic tv) =>
Bool
-> ([Symbol] -> v1 -> m v2)
-> ([Symbol] -> r1 -> m r2)
-> [Symbol]
-> RTypeV v1 c tv r1
-> m (RTypeV v2 c tv r2)
emapReftM Bool
bscp [Symbol] -> v1 -> m v2
vf [Symbol] -> r1 -> m r2
f = [Symbol] -> RTypeV v1 c tv r1 -> m (RTypeV v2 c tv r2)
forall {a} {c}.
Symbolic a =>
[Symbol] -> RTypeV v1 c a r1 -> m (RTypeV v2 c a r2)
go
  where
    go :: [Symbol] -> RTypeV v1 c a r1 -> m (RTypeV v2 c a r2)
go [Symbol]
γ (RVar a
α r1
r)        = a -> r2 -> RTypeV v2 c a r2
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar  a
α (r2 -> RTypeV v2 c a r2) -> m r2 -> m (RTypeV v2 c a r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> r1 -> m r2
f [Symbol]
γ r1
r
    go [Symbol]
γ (RAllT RTVUV v1 c a
α RTypeV v1 c a r1
t r1
r)     = RTVUV v2 c a -> RTypeV v2 c a r2 -> r2 -> RTypeV v2 c a r2
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT (RTVUV v2 c a -> RTypeV v2 c a r2 -> r2 -> RTypeV v2 c a r2)
-> m (RTVUV v2 c a)
-> m (RTypeV v2 c a r2 -> r2 -> RTypeV v2 c a r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RTypeV v1 c a () -> m (RTypeV v2 c a ()))
-> RTVUV v1 c a -> m (RTVUV v2 c a)
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 a a -> f (RTVar a b)
traverse (Bool
-> ([Symbol] -> v1 -> m v2)
-> ([Symbol] -> () -> m ())
-> [Symbol]
-> RTypeV v1 c a ()
-> m (RTypeV v2 c a ())
forall (m :: * -> *) r1 tv v1 v2 r2 c.
(Monad m, ToReftV r1, Symbolic tv) =>
Bool
-> ([Symbol] -> v1 -> m v2)
-> ([Symbol] -> r1 -> m r2)
-> [Symbol]
-> RTypeV v1 c tv r1
-> m (RTypeV v2 c tv r2)
emapReftM Bool
bscp [Symbol] -> v1 -> m v2
vf ((() -> m ()) -> [Symbol] -> () -> m ()
forall a b. a -> b -> a
const () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure) [Symbol]
γ) RTVUV v1 c a
α m (RTypeV v2 c a r2 -> r2 -> RTypeV v2 c a r2)
-> m (RTypeV v2 c a r2) -> m (r2 -> RTypeV v2 c a r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> RTypeV v1 c a r1 -> m (RTypeV v2 c a r2)
go (a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (RTVUV v1 c a -> a
forall tv s. RTVar tv s -> tv
ty_var_value RTVUV v1 c a
α) Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
γ) RTypeV v1 c a r1
t m (r2 -> RTypeV v2 c a r2) -> m r2 -> m (RTypeV v2 c a r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r1 -> m r2
f [Symbol]
γ r1
r
    go [Symbol]
γ (RAllP PVUV v1 c a
π RTypeV v1 c a r1
t)       = PVUV v2 c a -> RTypeV v2 c a r2 -> RTypeV v2 c a r2
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP (PVUV v2 c a -> RTypeV v2 c a r2 -> RTypeV v2 c a r2)
-> m (PVUV v2 c a) -> m (RTypeV v2 c a r2 -> RTypeV v2 c a r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Symbol] -> v1 -> m v2)
-> ([Symbol] -> RTypeV v1 c a () -> m (RTypeV v2 c a ()))
-> PVUV v1 c a
-> m (PVUV v2 c a)
forall (m :: * -> *) v v' t t'.
Monad m =>
([Symbol] -> v -> m v')
-> ([Symbol] -> t -> m t') -> PVarV v t -> m (PVarV v' t')
emapPVarVM [Symbol] -> v1 -> m v2
vf (Bool
-> ([Symbol] -> v1 -> m v2)
-> ([Symbol] -> () -> m ())
-> [Symbol]
-> RTypeV v1 c a ()
-> m (RTypeV v2 c a ())
forall (m :: * -> *) r1 tv v1 v2 r2 c.
(Monad m, ToReftV r1, Symbolic tv) =>
Bool
-> ([Symbol] -> v1 -> m v2)
-> ([Symbol] -> r1 -> m r2)
-> [Symbol]
-> RTypeV v1 c tv r1
-> m (RTypeV v2 c tv r2)
emapReftM Bool
bscp [Symbol] -> v1 -> m v2
vf ((() -> m ()) -> [Symbol] -> () -> m ()
forall a b. a -> b -> a
const () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure)) PVUV v1 c a
π m (RTypeV v2 c a r2 -> RTypeV v2 c a r2)
-> m (RTypeV v2 c a r2) -> m (RTypeV v2 c a r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> RTypeV v1 c a r1 -> m (RTypeV v2 c a r2)
go [Symbol]
γ RTypeV v1 c a r1
t
    go [Symbol]
γ (RFun Symbol
x RFInfo
i RTypeV v1 c a r1
t RTypeV v1 c a r1
t' r1
r) = Symbol
-> RFInfo
-> RTypeV v2 c a r2
-> RTypeV v2 c a r2
-> r2
-> RTypeV v2 c a r2
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun  Symbol
x RFInfo
i (RTypeV v2 c a r2 -> RTypeV v2 c a r2 -> r2 -> RTypeV v2 c a r2)
-> m (RTypeV v2 c a r2)
-> m (RTypeV v2 c a r2 -> r2 -> RTypeV v2 c a r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> RTypeV v1 c a r1 -> m (RTypeV v2 c a r2)
go (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
γ) RTypeV v1 c a r1
t m (RTypeV v2 c a r2 -> r2 -> RTypeV v2 c a r2)
-> m (RTypeV v2 c a r2) -> m (r2 -> RTypeV v2 c a r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> RTypeV v1 c a r1 -> m (RTypeV v2 c a r2)
go (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
γ) RTypeV v1 c a r1
t' m (r2 -> RTypeV v2 c a r2) -> m r2 -> m (RTypeV v2 c a r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r1 -> m r2
f (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
γ) r1
r
    go [Symbol]
γ (RApp c
c [RTypeV v1 c a r1]
ts [RTPropV v1 c a r1]
rs r1
r)  =
      let γ' :: [Symbol]
γ' = if Bool
bscp then ReftV (ReftVar r1) -> Symbol
forall v. ReftV v -> Symbol
F.reftBind (r1 -> ReftV (ReftVar r1)
forall r. ToReftV r => r -> ReftV (ReftVar r)
toReftV r1
r) Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
γ  else [Symbol]
γ
       in c
-> [RTypeV v2 c a r2]
-> [RTPropV v2 c a r2]
-> r2
-> RTypeV v2 c a r2
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp  c
c ([RTypeV v2 c a r2]
 -> [RTPropV v2 c a r2] -> r2 -> RTypeV v2 c a r2)
-> m [RTypeV v2 c a r2]
-> m ([RTPropV v2 c a r2] -> r2 -> RTypeV v2 c a r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (RTypeV v1 c a r1 -> m (RTypeV v2 c a r2))
-> [RTypeV v1 c a r1] -> m [RTypeV v2 c a 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 ([Symbol] -> RTypeV v1 c a r1 -> m (RTypeV v2 c a r2)
go [Symbol]
γ') [RTypeV v1 c a r1]
ts m ([RTPropV v2 c a r2] -> r2 -> RTypeV v2 c a r2)
-> m [RTPropV v2 c a r2] -> m (r2 -> RTypeV v2 c a r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (RTPropV v1 c a r1 -> m (RTPropV v2 c a r2))
-> [RTPropV v1 c a r1] -> m [RTPropV v2 c a 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
-> ([Symbol] -> v1 -> m v2)
-> ([Symbol] -> r1 -> m r2)
-> [Symbol]
-> RTPropV v1 c a r1
-> m (RTPropV v2 c a r2)
forall (m :: * -> *) t tv v v' s c.
(Monad m, ToReftV t, Symbolic tv) =>
Bool
-> ([Symbol] -> v -> m v')
-> ([Symbol] -> t -> m s)
-> [Symbol]
-> RTPropV v c tv t
-> m (RTPropV v' c tv s)
emapRefM Bool
bscp [Symbol] -> v1 -> m v2
vf [Symbol] -> r1 -> m r2
f [Symbol]
γ) [RTPropV v1 c a r1]
rs m (r2 -> RTypeV v2 c a r2) -> m r2 -> m (RTypeV v2 c a r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r1 -> m r2
f [Symbol]
γ r1
r
    go [Symbol]
γ (RAllE Symbol
z RTypeV v1 c a r1
t RTypeV v1 c a r1
t')    = Symbol -> RTypeV v2 c a r2 -> RTypeV v2 c a r2 -> RTypeV v2 c a r2
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
RAllE Symbol
z (RTypeV v2 c a r2 -> RTypeV v2 c a r2 -> RTypeV v2 c a r2)
-> m (RTypeV v2 c a r2) -> m (RTypeV v2 c a r2 -> RTypeV v2 c a r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> RTypeV v1 c a r1 -> m (RTypeV v2 c a r2)
go [Symbol]
γ RTypeV v1 c a r1
t m (RTypeV v2 c a r2 -> RTypeV v2 c a r2)
-> m (RTypeV v2 c a r2) -> m (RTypeV v2 c a r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> RTypeV v1 c a r1 -> m (RTypeV v2 c a r2)
go [Symbol]
γ RTypeV v1 c a r1
t'
    go [Symbol]
γ (REx Symbol
z RTypeV v1 c a r1
t RTypeV v1 c a r1
t')      = Symbol -> RTypeV v2 c a r2 -> RTypeV v2 c a r2 -> RTypeV v2 c a r2
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
REx   Symbol
z (RTypeV v2 c a r2 -> RTypeV v2 c a r2 -> RTypeV v2 c a r2)
-> m (RTypeV v2 c a r2) -> m (RTypeV v2 c a r2 -> RTypeV v2 c a r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> RTypeV v1 c a r1 -> m (RTypeV v2 c a r2)
go [Symbol]
γ RTypeV v1 c a r1
t m (RTypeV v2 c a r2 -> RTypeV v2 c a r2)
-> m (RTypeV v2 c a r2) -> m (RTypeV v2 c a r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> RTypeV v1 c a r1 -> m (RTypeV v2 c a r2)
go [Symbol]
γ RTypeV v1 c a r1
t'
    go [Symbol]
γ (RExprArg Located (ExprV v1)
e)      = Located (ExprV v2) -> RTypeV v2 c a r2
forall v c tv r. Located (ExprV v) -> RTypeV v c tv r
RExprArg (Located (ExprV v2) -> RTypeV v2 c a r2)
-> m (Located (ExprV v2)) -> m (RTypeV v2 c a r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ExprV v1 -> m (ExprV v2))
-> Located (ExprV v1) -> m (Located (ExprV 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 (([Symbol] -> v1 -> m v2) -> ExprV v1 -> m (ExprV v2)
forall (m :: * -> *) v v'.
Monad m =>
([Symbol] -> v -> m v') -> ExprV v -> m (ExprV v')
emapExprVM ([Symbol] -> v1 -> m v2
vf ([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]
γ))) Located (ExprV v1)
e
    go [Symbol]
γ (RAppTy RTypeV v1 c a r1
t RTypeV v1 c a r1
t' r1
r)   = RTypeV v2 c a r2 -> RTypeV v2 c a r2 -> r2 -> RTypeV v2 c a r2
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy (RTypeV v2 c a r2 -> RTypeV v2 c a r2 -> r2 -> RTypeV v2 c a r2)
-> m (RTypeV v2 c a r2)
-> m (RTypeV v2 c a r2 -> r2 -> RTypeV v2 c a r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> RTypeV v1 c a r1 -> m (RTypeV v2 c a r2)
go [Symbol]
γ RTypeV v1 c a r1
t m (RTypeV v2 c a r2 -> r2 -> RTypeV v2 c a r2)
-> m (RTypeV v2 c a r2) -> m (r2 -> RTypeV v2 c a r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> RTypeV v1 c a r1 -> m (RTypeV v2 c a r2)
go [Symbol]
γ RTypeV v1 c a r1
t' m (r2 -> RTypeV v2 c a r2) -> m r2 -> m (RTypeV v2 c a r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r1 -> m r2
f [Symbol]
γ r1
r
    go [Symbol]
γ (RRTy [(Symbol, RTypeV v1 c a r1)]
e r1
r Oblig
o RTypeV v1 c a r1
t)    =
      [(Symbol, RTypeV v2 c a r2)]
-> r2 -> Oblig -> RTypeV v2 c a r2 -> RTypeV v2 c a r2
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy ([(Symbol, RTypeV v2 c a r2)]
 -> r2 -> Oblig -> RTypeV v2 c a r2 -> RTypeV v2 c a r2)
-> m [(Symbol, RTypeV v2 c a r2)]
-> m (r2 -> Oblig -> RTypeV v2 c a r2 -> RTypeV v2 c a r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Symbol, RTypeV v1 c a r1) -> m (Symbol, RTypeV v2 c a r2))
-> [(Symbol, RTypeV v1 c a r1)] -> m [(Symbol, RTypeV v2 c a 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 ((RTypeV v1 c a r1 -> m (RTypeV v2 c a r2))
-> (Symbol, RTypeV v1 c a r1) -> m (Symbol, RTypeV v2 c a 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 ([Symbol] -> RTypeV v1 c a r1 -> m (RTypeV v2 c a r2)
go (((Symbol, RTypeV v1 c a r1) -> Symbol)
-> [(Symbol, RTypeV v1 c a r1)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, RTypeV v1 c a r1) -> Symbol
forall a b. (a, b) -> a
fst [(Symbol, RTypeV v1 c a r1)]
e [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
γ))) [(Symbol, RTypeV v1 c a r1)]
e m (r2 -> Oblig -> RTypeV v2 c a r2 -> RTypeV v2 c a r2)
-> m r2 -> m (Oblig -> RTypeV v2 c a r2 -> RTypeV v2 c a r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> r1 -> m r2
f [Symbol]
γ r1
r m (Oblig -> RTypeV v2 c a r2 -> RTypeV v2 c a r2)
-> m Oblig -> m (RTypeV v2 c a r2 -> RTypeV v2 c a 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 (RTypeV v2 c a r2 -> RTypeV v2 c a r2)
-> m (RTypeV v2 c a r2) -> m (RTypeV v2 c a r2)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Symbol] -> RTypeV v1 c a r1 -> m (RTypeV v2 c a r2)
go [Symbol]
γ RTypeV v1 c a r1
t
    go [Symbol]
γ (RHole r1
r)         = r2 -> RTypeV v2 c a r2
forall v c tv r. r -> RTypeV v c tv r
RHole (r2 -> RTypeV v2 c a r2) -> m r2 -> m (RTypeV v2 c a r2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> r1 -> m r2
f [Symbol]
γ r1
r

emapRefM
  :: (Monad m, ToReftV t, F.Symbolic tv)
  => Bool
  -> ([Symbol] -> v -> m v')
  -> ([Symbol] -> t -> m s)
  -> [Symbol]
  -> RTPropV v c tv t
  -> m (RTPropV v' c tv s)
emapRefM :: forall (m :: * -> *) t tv v v' s c.
(Monad m, ToReftV t, Symbolic tv) =>
Bool
-> ([Symbol] -> v -> m v')
-> ([Symbol] -> t -> m s)
-> [Symbol]
-> RTPropV v c tv t
-> m (RTPropV v' c tv s)
emapRefM Bool
bscp [Symbol] -> v -> m v'
vf [Symbol] -> t -> m s
f [Symbol]
γ0 (RProp [(Symbol, RTypeV v c tv ())]
ss RTypeV v c tv t
t0) =
    [(Symbol, RTypeV v' c tv ())]
-> RTypeV v' c tv s -> Ref (RTypeV v' c tv ()) (RTypeV v' c tv s)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp ([(Symbol, RTypeV v' c tv ())]
 -> RTypeV v' c tv s -> Ref (RTypeV v' c tv ()) (RTypeV v' c tv s))
-> (([Symbol], [(Symbol, RTypeV v' c tv ())])
    -> [(Symbol, RTypeV v' c tv ())])
-> ([Symbol], [(Symbol, RTypeV v' c tv ())])
-> RTypeV v' c tv s
-> Ref (RTypeV v' c tv ()) (RTypeV v' c tv s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Symbol], [(Symbol, RTypeV v' c tv ())])
-> [(Symbol, RTypeV v' c tv ())]
forall a b. (a, b) -> b
snd (([Symbol], [(Symbol, RTypeV v' c tv ())])
 -> RTypeV v' c tv s -> Ref (RTypeV v' c tv ()) (RTypeV v' c tv s))
-> m ([Symbol], [(Symbol, RTypeV v' c tv ())])
-> m (RTypeV v' c tv s
      -> Ref (RTypeV v' c tv ()) (RTypeV v' c tv s))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      ([Symbol]
 -> (Symbol, RTypeV v c tv ())
 -> m ([Symbol], (Symbol, RTypeV v' c tv ())))
-> [Symbol]
-> [(Symbol, RTypeV v c tv ())]
-> m ([Symbol], [(Symbol, RTypeV v' c tv ())])
forall (m :: * -> *) (t :: * -> *) a b c.
(Monad m, Traversable t) =>
(a -> b -> m (a, c)) -> a -> t b -> m (a, t c)
mapAccumM
        (\[Symbol]
γ (Symbol
s, RTypeV v c tv ()
t) -> (Symbol
sSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
γ,) ((Symbol, RTypeV v' c tv ())
 -> ([Symbol], (Symbol, RTypeV v' c tv ())))
-> (RTypeV v' c tv () -> (Symbol, RTypeV v' c tv ()))
-> RTypeV v' c tv ()
-> ([Symbol], (Symbol, RTypeV v' c tv ()))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol
s,) (RTypeV v' c tv () -> ([Symbol], (Symbol, RTypeV v' c tv ())))
-> m (RTypeV v' c tv ())
-> m ([Symbol], (Symbol, RTypeV v' c tv ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> ([Symbol] -> v -> m v')
-> ([Symbol] -> () -> m ())
-> [Symbol]
-> RTypeV v c tv ()
-> m (RTypeV v' c tv ())
forall (m :: * -> *) r1 tv v1 v2 r2 c.
(Monad m, ToReftV r1, Symbolic tv) =>
Bool
-> ([Symbol] -> v1 -> m v2)
-> ([Symbol] -> r1 -> m r2)
-> [Symbol]
-> RTypeV v1 c tv r1
-> m (RTypeV v2 c tv r2)
emapReftM Bool
bscp [Symbol] -> v -> m v'
vf ((() -> m ()) -> [Symbol] -> () -> m ()
forall a b. a -> b -> a
const () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure) [Symbol]
γ RTypeV v c tv ()
t)
        [Symbol]
γ0
        [(Symbol, RTypeV v c tv ())]
ss
      m (RTypeV v' c tv s -> Ref (RTypeV v' c tv ()) (RTypeV v' c tv s))
-> m (RTypeV v' c tv s)
-> m (Ref (RTypeV v' c tv ()) (RTypeV 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
-> ([Symbol] -> v -> m v')
-> ([Symbol] -> t -> m s)
-> [Symbol]
-> RTypeV v c tv t
-> m (RTypeV v' c tv s)
forall (m :: * -> *) r1 tv v1 v2 r2 c.
(Monad m, ToReftV r1, Symbolic tv) =>
Bool
-> ([Symbol] -> v1 -> m v2)
-> ([Symbol] -> r1 -> m r2)
-> [Symbol]
-> RTypeV v1 c tv r1
-> m (RTypeV v2 c tv r2)
emapReftM Bool
bscp [Symbol] -> v -> m v'
vf [Symbol] -> t -> m s
f (((Symbol, RTypeV v c tv ()) -> Symbol)
-> [(Symbol, RTypeV v c tv ())] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, RTypeV v c tv ()) -> Symbol
forall a b. (a, b) -> a
fst [(Symbol, RTypeV v c tv ())]
ss [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
γ0) RTypeV v c tv t
t0

emapBareTypeVM
  :: Monad m
  => Bool
  -> ([Symbol] -> v1 -> m v2)
  -> [Symbol]
  -> BareTypeV v1
  -> m (BareTypeV v2)
emapBareTypeVM :: forall (m :: * -> *) v1 v2.
Monad m =>
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]
-> RTypeV v1 BTyCon BTyVar (RReftV v1)
-> m (RTypeV v2 BTyCon BTyVar (RReftV v2))
forall (m :: * -> *) r1 tv v1 v2 r2 c.
(Monad m, ToReftV r1, Symbolic tv) =>
Bool
-> ([Symbol] -> v1 -> m v2)
-> ([Symbol] -> r1 -> m r2)
-> [Symbol]
-> RTypeV v1 c tv r1
-> m (RTypeV v2 c tv r2)
emapReftM
      Bool
bscp
      [Symbol] -> v1 -> m v2
f
      (\[Symbol]
e -> ([Symbol] -> v1 -> m v2)
-> (ReftV v1 -> m (ReftV 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) -> ReftV v1 -> m (ReftV 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'.
(v -> v') -> (t -> t') -> PVarV v t -> PVarV v' t'
mapPVarV v -> v'
f ((v -> v') -> BSortV v -> BSortV v'
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV 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 <- (PVarV v (RTypeV v BTyCon BTyVar ())
 -> m (PVarV v' (RTypeV v' BTyCon BTyVar ())))
-> [PVarV v (RTypeV v BTyCon BTyVar ())]
-> m [PVarV v' (RTypeV v' BTyCon BTyVar ())]
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]
    -> RTypeV v BTyCon BTyVar () -> m (RTypeV v' BTyCon BTyVar ()))
-> PVarV v (RTypeV v BTyCon BTyVar ())
-> m (PVarV v' (RTypeV v' BTyCon BTyVar ()))
forall (m :: * -> *) v v' t t'.
Monad m =>
([Symbol] -> v -> m v')
-> ([Symbol] -> t -> m t') -> PVarV v t -> m (PVarV v' t')
emapPVarVM [Symbol] -> v -> m v'
vf (Bool
-> ([Symbol] -> v -> m v')
-> ([Symbol] -> () -> m ())
-> [Symbol]
-> RTypeV v BTyCon BTyVar ()
-> m (RTypeV v' BTyCon BTyVar ())
forall (m :: * -> *) r1 tv v1 v2 r2 c.
(Monad m, ToReftV r1, Symbolic tv) =>
Bool
-> ([Symbol] -> v1 -> m v2)
-> ([Symbol] -> r1 -> m r2)
-> [Symbol]
-> RTypeV v1 c tv r1
-> m (RTypeV v2 c tv r2)
emapReftM Bool
bscp [Symbol] -> v -> m v'
vf ((() -> m ()) -> [Symbol] -> () -> m ()
forall a b. a -> b -> a
const () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure))) ([PVarV v (RTypeV v BTyCon BTyVar ())]
 -> m [PVarV v' (RTypeV v' BTyCon BTyVar ())])
-> [PVarV v (RTypeV v BTyCon BTyVar ())]
-> m [PVarV v' (RTypeV v' BTyCon BTyVar ())]
forall a b. (a -> b) -> a -> b
$ DataDeclP v ty -> [PVarV v (RTypeV v BTyCon BTyVar ())]
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 :: ([Symbol] -> Expr -> Expr) -> [Symbol] -> RType c tv r -> RType c tv r
emapExprArg :: forall c tv r.
([Symbol] -> ExprV Symbol -> ExprV Symbol)
-> [Symbol] -> RType c tv r -> RType c tv r
emapExprArg [Symbol] -> ExprV Symbol -> ExprV Symbol
f = [Symbol] -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall {c} {tv} {r}.
[Symbol] -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go
  where
    go :: [Symbol] -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go [Symbol]
_ t :: RTypeV Symbol c tv r
t@RVar{}          = RTypeV Symbol c tv r
t
    go [Symbol]
_ t :: RTypeV Symbol c tv r
t@RHole{}         = RTypeV Symbol c tv r
t
    go [Symbol]
γ (RAllT RTVUV Symbol c tv
α RTypeV Symbol c tv r
t r
r)     = RTVUV Symbol c tv
-> RTypeV Symbol c tv r -> r -> RTypeV Symbol c tv r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV Symbol c tv
α ([Symbol] -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go [Symbol]
γ RTypeV Symbol c tv r
t) r
r
    go [Symbol]
γ (RAllP PVUV Symbol c tv
π RTypeV Symbol c tv r
t)       = PVUV Symbol c tv -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV Symbol c tv
π ([Symbol] -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go [Symbol]
γ RTypeV Symbol c tv r
t)
    go [Symbol]
γ (RFun Symbol
x RFInfo
i RTypeV Symbol c tv r
t RTypeV Symbol c tv r
t' r
r) = Symbol
-> RFInfo
-> RTypeV Symbol c tv r
-> RTypeV Symbol c tv r
-> r
-> RTypeV Symbol c tv r
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun  Symbol
x RFInfo
i ([Symbol] -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go [Symbol]
γ RTypeV Symbol c tv r
t) ([Symbol] -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go (Symbol
xSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
γ) RTypeV Symbol c tv r
t') r
r
    go [Symbol]
γ (RApp c
c [RTypeV Symbol c tv r]
ts [RTPropV Symbol c tv r]
rs r
r)  = c
-> [RTypeV Symbol c tv r]
-> [RTPropV Symbol c tv r]
-> r
-> RTypeV Symbol c tv r
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp  c
c ([Symbol] -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go [Symbol]
γ (RTypeV Symbol c tv r -> RTypeV Symbol c tv r)
-> [RTypeV Symbol c tv r] -> [RTypeV Symbol c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeV Symbol c tv r]
ts) ([Symbol] -> RTPropV Symbol c tv r -> RTPropV Symbol c tv r
mo [Symbol]
γ (RTPropV Symbol c tv r -> RTPropV Symbol c tv r)
-> [RTPropV Symbol c tv r] -> [RTPropV Symbol c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropV Symbol c tv r]
rs) r
r
    go [Symbol]
γ (RAllE Symbol
z RTypeV Symbol c tv r
t RTypeV Symbol c tv r
t')    = Symbol
-> RTypeV Symbol c tv r
-> RTypeV Symbol c tv r
-> RTypeV Symbol c tv r
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
RAllE Symbol
z ([Symbol] -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go [Symbol]
γ RTypeV Symbol c tv r
t) ([Symbol] -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go [Symbol]
γ RTypeV Symbol c tv r
t')
    go [Symbol]
γ (REx Symbol
z RTypeV Symbol c tv r
t RTypeV Symbol c tv r
t')      = Symbol
-> RTypeV Symbol c tv r
-> RTypeV Symbol c tv r
-> RTypeV Symbol c tv r
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
REx   Symbol
z ([Symbol] -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go [Symbol]
γ RTypeV Symbol c tv r
t) ([Symbol] -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go [Symbol]
γ RTypeV Symbol c tv r
t')
    go [Symbol]
γ (RExprArg Located (ExprV Symbol)
e)      = Located (ExprV Symbol) -> RTypeV Symbol c tv r
forall v c tv r. Located (ExprV v) -> RTypeV v c tv r
RExprArg ([Symbol] -> ExprV Symbol -> ExprV Symbol
f [Symbol]
γ (ExprV Symbol -> ExprV Symbol)
-> Located (ExprV Symbol) -> Located (ExprV Symbol)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> Located (ExprV Symbol) -> Located (ExprV Symbol)
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"RExprArg" Located (ExprV Symbol)
e) -- <---- actual substitution
    go [Symbol]
γ (RAppTy RTypeV Symbol c tv r
t RTypeV Symbol c tv r
t' r
r)   = RTypeV Symbol c tv r
-> RTypeV Symbol c tv r -> r -> RTypeV Symbol c tv r
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy ([Symbol] -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go [Symbol]
γ RTypeV Symbol c tv r
t) ([Symbol] -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go [Symbol]
γ RTypeV Symbol c tv r
t') r
r
    go [Symbol]
γ (RRTy [(Symbol, RTypeV Symbol c tv r)]
e r
r Oblig
o RTypeV Symbol c tv r
t)    = [(Symbol, RTypeV Symbol c tv r)]
-> r -> Oblig -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy  ((RTypeV Symbol c tv r -> RTypeV Symbol c tv r)
-> (Symbol, RTypeV Symbol c tv r) -> (Symbol, RTypeV 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 ([Symbol] -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go [Symbol]
γ) ((Symbol, RTypeV Symbol c tv r) -> (Symbol, RTypeV Symbol c tv r))
-> [(Symbol, RTypeV Symbol c tv r)]
-> [(Symbol, RTypeV Symbol c tv r)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RTypeV Symbol c tv r)]
e) r
r Oblig
o ([Symbol] -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go [Symbol]
γ RTypeV Symbol c tv r
t)

    mo :: [Symbol] -> RTPropV Symbol c tv r -> RTPropV Symbol c tv r
mo [Symbol]
_ t :: RTPropV Symbol c tv r
t@(RProp [(Symbol, RTypeV Symbol c tv ())]
_ RHole{}) = RTPropV Symbol c tv r
t
    mo [Symbol]
γ (RProp [(Symbol, RTypeV Symbol c tv ())]
s RTypeV Symbol c tv r
t)         = [(Symbol, RTypeV Symbol c tv ())]
-> RTypeV Symbol c tv r -> RTPropV Symbol c tv r
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RTypeV Symbol c tv ())]
s ([Symbol] -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
go [Symbol]
γ RTypeV Symbol c tv r
t)

parsedToBareType :: BareTypeParsed -> BareType
parsedToBareType :: BareTypeParsed -> BareType
parsedToBareType = (Located Symbol -> Symbol)
-> RTypeV (Located Symbol) BTyCon BTyVar RReft -> BareType
forall v v' c tv r.
(v -> v') -> RTypeV v c tv r -> RTypeV v' c tv r
mapRTypeV Located Symbol -> Symbol
forall a. Located a -> a
F.val (RTypeV (Located Symbol) BTyCon BTyVar RReft -> BareType)
-> (BareTypeParsed -> RTypeV (Located Symbol) BTyCon BTyVar RReft)
-> BareTypeParsed
-> BareType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RReftV (Located Symbol) -> RReft)
-> BareTypeParsed -> RTypeV (Located Symbol) BTyCon BTyVar RReft
forall r1 r2 v c tv.
(r1 -> r2) -> RTypeV v c tv r1 -> RTypeV v c tv r2
mapReft ((Located Symbol -> Symbol)
-> (ReftV (Located Symbol) -> ReftV 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)
-> ReftV (Located Symbol) -> ReftV Symbol
forall a b. (a -> b) -> ReftV a -> ReftV 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 -> RTPropV Symbol c tv r -> acc
prep acc
a (RProp [(Symbol, RTypeV Symbol c tv ())]
_ RHole{}) = acc
a
    prep acc
a (RProp [(Symbol, RTypeV Symbol c tv ())]
_ 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 RTVUV 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 PVUV 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 [RTPropV Symbol c tv r]
rs r
_)   = (acc -> RTPropV Symbol c tv r -> acc)
-> acc -> [RTPropV 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 -> RTPropV 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) [RTPropV 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 RTVUV Symbol t t1
_ RTypeV Symbol t t1 t2
t t2
_)    = RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase RTypeV Symbol t t1 t2
t
isBase (RAllP PVUV Symbol t t1
_ RTypeV Symbol t t1 t2
t)      = RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase RTypeV Symbol t t1 t2
t
isBase (RVar t1
_ t2
_)       = Bool
True
isBase (RApp t
_ [RTypeV Symbol t t1 t2]
ts [RTPropV Symbol t t1 t2]
_ t2
_)  = (RTypeV Symbol t t1 t2 -> Bool) -> [RTypeV Symbol t t1 t2] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase [RTypeV Symbol t t1 t2]
ts
isBase RFun{}           = Bool
False
isBase (RAppTy RTypeV Symbol t t1 t2
t1 RTypeV Symbol t t1 t2
t2 t2
_) = RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase RTypeV Symbol t t1 t2
t1 Bool -> Bool -> Bool
&& RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase RTypeV Symbol t t1 t2
t2
isBase (RRTy [(Symbol, RTypeV Symbol t t1 t2)]
_ t2
_ Oblig
_ RTypeV Symbol t t1 t2
t)   = RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase RTypeV Symbol t t1 t2
t
isBase (RAllE Symbol
_ RTypeV Symbol t t1 t2
_ RTypeV Symbol t t1 t2
t)    = RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase RTypeV Symbol t t1 t2
t
isBase (REx Symbol
_ RTypeV Symbol t t1 t2
_ RTypeV Symbol t t1 t2
t)      = RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isBase RTypeV Symbol t t1 t2
t
isBase RTypeV 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 RTVUV Symbol t t1
_ RTypeV Symbol t t1 t2
t t2
_)     = RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeV Symbol t t1 t2
t
hasHoleTy (RAllP PVUV Symbol t t1
_ RTypeV Symbol t t1 t2
t)       = RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeV Symbol t t1 t2
t
hasHoleTy (RFun Symbol
_ RFInfo
_ RTypeV Symbol t t1 t2
t RTypeV Symbol t t1 t2
t' t2
_) = RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeV Symbol t t1 t2
t Bool -> Bool -> Bool
|| RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeV Symbol t t1 t2
t'
hasHoleTy (RApp t
_ [RTypeV Symbol t t1 t2]
ts [RTPropV Symbol t t1 t2]
_ t2
_)   = (RTypeV Symbol t t1 t2 -> Bool) -> [RTypeV Symbol t t1 t2] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy [RTypeV Symbol t t1 t2]
ts
hasHoleTy (RAllE Symbol
_ RTypeV Symbol t t1 t2
t RTypeV Symbol t t1 t2
t')    = RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeV Symbol t t1 t2
t Bool -> Bool -> Bool
|| RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeV Symbol t t1 t2
t'
hasHoleTy (REx Symbol
_ RTypeV Symbol t t1 t2
t RTypeV Symbol t t1 t2
t')      = RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeV Symbol t t1 t2
t Bool -> Bool -> Bool
|| RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeV Symbol t t1 t2
t'
hasHoleTy (RExprArg Located (ExprV Symbol)
_)      = Bool
False
hasHoleTy (RAppTy RTypeV Symbol t t1 t2
t RTypeV Symbol t t1 t2
t' t2
_)   = RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeV Symbol t t1 t2
t Bool -> Bool -> Bool
|| RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeV Symbol t t1 t2
t'
hasHoleTy (RHole t2
_)         = Bool
True
hasHoleTy (RRTy [(Symbol, RTypeV Symbol t t1 t2)]
xts t2
_ Oblig
_ RTypeV Symbol t t1 t2
t)  = RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy RTypeV Symbol t t1 t2
t Bool -> Bool -> Bool
|| (RTypeV Symbol t t1 t2 -> Bool) -> [RTypeV Symbol t t1 t2] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy ((Symbol, RTypeV Symbol t t1 t2) -> RTypeV Symbol t t1 t2
forall a b. (a, b) -> b
snd ((Symbol, RTypeV Symbol t t1 t2) -> RTypeV Symbol t t1 t2)
-> [(Symbol, RTypeV Symbol t t1 t2)] -> [RTypeV Symbol t t1 t2]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RTypeV Symbol t t1 t2)]
xts)

isFunTy :: RType t t1 t2 -> Bool
isFunTy :: forall t t1 t2. RType t t1 t2 -> Bool
isFunTy (RAllE Symbol
_ RTypeV Symbol t t1 t2
_ RTypeV Symbol t t1 t2
t)    = RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isFunTy RTypeV Symbol t t1 t2
t
isFunTy (RAllT RTVUV Symbol t t1
_ RTypeV Symbol t t1 t2
t t2
_)    = RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isFunTy RTypeV Symbol t t1 t2
t
isFunTy (RAllP PVUV Symbol t t1
_ RTypeV Symbol t t1 t2
t)      = RTypeV Symbol t t1 t2 -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isFunTy RTypeV Symbol t t1 t2
t
isFunTy RFun{}           = Bool
True
isFunTy RTypeV 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 v c tv r. tv -> r -> RTypeV v c tv r
RVar  tv
α)  (r1 -> m r2
f r1
r)
mapReftM r1 -> m r2
f (RAllT RTVUV Symbol c tv
α RTypeV 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 (RTVUV Symbol c tv -> RType c tv r2 -> r2 -> RType c tv r2
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV Symbol c tv
α)  ((r1 -> m r2) -> RTypeV 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 RTypeV Symbol c tv r1
t)         (r1 -> m r2
f r1
r)
mapReftM r1 -> m r2
f (RAllP PVUV Symbol c tv
π RTypeV 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   (PVUV Symbol c tv -> RType c tv r2 -> RType c tv r2
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV Symbol c tv
π)  ((r1 -> m r2) -> RTypeV 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 RTypeV Symbol c tv r1
t)
mapReftM r1 -> m r2
f (RFun Symbol
x RFInfo
i RTypeV Symbol c tv r1
t RTypeV 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 v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
x RFInfo
i) ((r1 -> m r2) -> RTypeV 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 RTypeV Symbol c tv r1
t)         ((r1 -> m r2) -> RTypeV 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 RTypeV Symbol c tv r1
t')       (r1 -> m r2
f r1
r)
mapReftM r1 -> m r2
f (RApp c
c [RTypeV Symbol c tv r1]
ts [RTPropV Symbol c tv r1]
rs r1
r)  = ([RType c tv r2]
 -> [RTPropV Symbol c tv r2] -> r2 -> RType c tv r2)
-> m [RType c tv r2]
-> m [RTPropV 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]
-> [RTPropV Symbol c tv r2]
-> r2
-> RType c tv r2
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp  c
c)  ((RTypeV Symbol c tv r1 -> m (RType c tv r2))
-> [RTypeV 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) -> RTypeV 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) [RTypeV Symbol c tv r1]
ts) ((RTPropV Symbol c tv r1 -> m (RTPropV Symbol c tv r2))
-> [RTPropV Symbol c tv r1] -> m [RTPropV 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)
-> RTPropV Symbol c tv r1 -> m (RTPropV 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) [RTPropV Symbol c tv r1]
rs) (r1 -> m r2
f r1
r)
mapReftM r1 -> m r2
f (RAllE Symbol
z RTypeV Symbol c tv r1
t RTypeV 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 v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
RAllE Symbol
z)  ((r1 -> m r2) -> RTypeV 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 RTypeV Symbol c tv r1
t)         ((r1 -> m r2) -> RTypeV 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 RTypeV Symbol c tv r1
t')
mapReftM r1 -> m r2
f (REx Symbol
z RTypeV Symbol c tv r1
t RTypeV 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 v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
REx Symbol
z)    ((r1 -> m r2) -> RTypeV 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 RTypeV Symbol c tv r1
t)         ((r1 -> m r2) -> RTypeV 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 RTypeV Symbol c tv r1
t')
mapReftM r1 -> m r2
_ (RExprArg Located (ExprV 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 (ExprV Symbol) -> RType c tv r2
forall v c tv r. Located (ExprV v) -> RTypeV v c tv r
RExprArg Located (ExprV Symbol)
e
mapReftM r1 -> m r2
f (RAppTy RTypeV Symbol c tv r1
t RTypeV 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 v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy ((r1 -> m r2) -> RTypeV 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 RTypeV Symbol c tv r1
t) ((r1 -> m r2) -> RTypeV 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 RTypeV 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 v c tv r. r -> RTypeV v c tv r
RHole      (r1 -> m r2
f r1
r)
mapReftM r1 -> m r2
f (RRTy [(Symbol, RTypeV Symbol c tv r1)]
xts r1
r Oblig
o RTypeV 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 v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy (((Symbol, RTypeV Symbol c tv r1) -> m (Symbol, RType c tv r2))
-> [(Symbol, RTypeV 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 ((RTypeV Symbol c tv r1 -> m (RType c tv r2))
-> (Symbol, RTypeV 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) -> RTypeV 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, RTypeV 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) -> RTypeV 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 RTypeV 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, RTypeV Symbol c tv ())]
s RTypeV Symbol c tv t
t)        = (RTypeV Symbol c tv s -> RTProp c tv s)
-> m (RTypeV 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, RTypeV Symbol c tv ())]
-> RTypeV Symbol c tv s -> RTProp c tv s
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RTypeV Symbol c tv ())]
s)      ((t -> m s) -> RTypeV Symbol c tv t -> m (RTypeV 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 RTypeV 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)        = RTypeV Symbol c tv r -> m (RTypeV Symbol c tv r)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (RTypeV Symbol c tv r -> m (RTypeV Symbol c tv r))
-> RTypeV Symbol c tv r -> m (RTypeV Symbol c tv r)
forall a b. (a -> b) -> a -> b
$ tv -> r -> RTypeV Symbol c tv r
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar  tv
α r
r
mapPropM RTProp c tv r -> m (RTProp c tv r)
f (RAllT RTVUV Symbol c tv
α RTypeV Symbol c tv r
t r
r)     = (RTypeV Symbol c tv r -> r -> RTypeV Symbol c tv r)
-> m (RTypeV Symbol c tv r) -> m r -> m (RTypeV Symbol c tv r)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (RTVUV Symbol c tv
-> RTypeV Symbol c tv r -> r -> RTypeV Symbol c tv r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV Symbol c tv
α)   ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeV Symbol c tv r -> m (RTypeV 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 RTypeV 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 PVUV Symbol c tv
π RTypeV Symbol c tv r
t)       = (RTypeV Symbol c tv r -> RTypeV Symbol c tv r)
-> m (RTypeV Symbol c tv r) -> m (RTypeV 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   (PVUV Symbol c tv -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV Symbol c tv
π)   ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeV Symbol c tv r -> m (RTypeV 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 RTypeV Symbol c tv r
t)
mapPropM RTProp c tv r -> m (RTProp c tv r)
f (RFun Symbol
x RFInfo
i RTypeV Symbol c tv r
t RTypeV Symbol c tv r
t' r
r) = (RTypeV Symbol c tv r
 -> RTypeV Symbol c tv r -> r -> RTypeV Symbol c tv r)
-> m (RTypeV Symbol c tv r)
-> m (RTypeV Symbol c tv r)
-> m r
-> m (RTypeV 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
-> RTypeV Symbol c tv r
-> RTypeV Symbol c tv r
-> r
-> RTypeV Symbol c tv r
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
x RFInfo
i)  ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeV Symbol c tv r -> m (RTypeV 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 RTypeV Symbol c tv r
t)          ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeV Symbol c tv r -> m (RTypeV 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 RTypeV 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 [RTypeV Symbol c tv r]
ts [RTProp c tv r]
rs r
r)  = ([RTypeV Symbol c tv r]
 -> [RTProp c tv r] -> r -> RTypeV Symbol c tv r)
-> m [RTypeV Symbol c tv r]
-> m [RTProp c tv r]
-> m r
-> m (RTypeV 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
-> [RTypeV Symbol c tv r]
-> [RTProp c tv r]
-> r
-> RTypeV Symbol c tv r
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp  c
c)   ((RTypeV Symbol c tv r -> m (RTypeV Symbol c tv r))
-> [RTypeV Symbol c tv r] -> m [RTypeV 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))
-> RTypeV Symbol c tv r -> m (RTypeV 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) [RTypeV 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 RTypeV Symbol c tv r
t RTypeV Symbol c tv r
t')    = (RTypeV Symbol c tv r
 -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r)
-> m (RTypeV Symbol c tv r)
-> m (RTypeV Symbol c tv r)
-> m (RTypeV Symbol c tv r)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Symbol
-> RTypeV Symbol c tv r
-> RTypeV Symbol c tv r
-> RTypeV Symbol c tv r
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
RAllE Symbol
z)   ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeV Symbol c tv r -> m (RTypeV 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 RTypeV Symbol c tv r
t)          ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeV Symbol c tv r -> m (RTypeV 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 RTypeV Symbol c tv r
t')
mapPropM RTProp c tv r -> m (RTProp c tv r)
f (REx Symbol
z RTypeV Symbol c tv r
t RTypeV Symbol c tv r
t')      = (RTypeV Symbol c tv r
 -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r)
-> m (RTypeV Symbol c tv r)
-> m (RTypeV Symbol c tv r)
-> m (RTypeV Symbol c tv r)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Symbol
-> RTypeV Symbol c tv r
-> RTypeV Symbol c tv r
-> RTypeV Symbol c tv r
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
REx Symbol
z)     ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeV Symbol c tv r -> m (RTypeV 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 RTypeV Symbol c tv r
t)          ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeV Symbol c tv r -> m (RTypeV 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 RTypeV Symbol c tv r
t')
mapPropM RTProp c tv r -> m (RTProp c tv r)
_ (RExprArg Located (ExprV Symbol)
e)      = RTypeV Symbol c tv r -> m (RTypeV Symbol c tv r)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (RTypeV Symbol c tv r -> m (RTypeV Symbol c tv r))
-> RTypeV Symbol c tv r -> m (RTypeV Symbol c tv r)
forall a b. (a -> b) -> a -> b
$ Located (ExprV Symbol) -> RTypeV Symbol c tv r
forall v c tv r. Located (ExprV v) -> RTypeV v c tv r
RExprArg Located (ExprV Symbol)
e
mapPropM RTProp c tv r -> m (RTProp c tv r)
f (RAppTy RTypeV Symbol c tv r
t RTypeV Symbol c tv r
t' r
r)   = (RTypeV Symbol c tv r
 -> RTypeV Symbol c tv r -> r -> RTypeV Symbol c tv r)
-> m (RTypeV Symbol c tv r)
-> m (RTypeV Symbol c tv r)
-> m r
-> m (RTypeV 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 RTypeV Symbol c tv r
-> RTypeV Symbol c tv r -> r -> RTypeV Symbol c tv r
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeV Symbol c tv r -> m (RTypeV 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 RTypeV Symbol c tv r
t) ((RTProp c tv r -> m (RTProp c tv r))
-> RTypeV Symbol c tv r -> m (RTypeV 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 RTypeV 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)         = RTypeV Symbol c tv r -> m (RTypeV Symbol c tv r)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (RTypeV Symbol c tv r -> m (RTypeV Symbol c tv r))
-> RTypeV Symbol c tv r -> m (RTypeV Symbol c tv r)
forall a b. (a -> b) -> a -> b
$ r -> RTypeV Symbol c tv r
forall v c tv r. r -> RTypeV v c tv r
RHole r
r
mapPropM RTProp c tv r -> m (RTProp c tv r)
f (RRTy [(Symbol, RTypeV Symbol c tv r)]
xts r
r Oblig
o RTypeV Symbol c tv r
t)  = ([(Symbol, RTypeV Symbol c tv r)]
 -> r -> Oblig -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r)
-> m [(Symbol, RTypeV Symbol c tv r)]
-> m r
-> m Oblig
-> m (RTypeV Symbol c tv r)
-> m (RTypeV 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, RTypeV Symbol c tv r)]
-> r -> Oblig -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy (((Symbol, RTypeV Symbol c tv r)
 -> m (Symbol, RTypeV Symbol c tv r))
-> [(Symbol, RTypeV Symbol c tv r)]
-> m [(Symbol, RTypeV 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 ((RTypeV Symbol c tv r -> m (RTypeV Symbol c tv r))
-> (Symbol, RTypeV Symbol c tv r)
-> m (Symbol, RTypeV 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))
-> RTypeV Symbol c tv r -> m (RTypeV 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, RTypeV 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))
-> RTypeV Symbol c tv r -> m (RTypeV 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 RTypeV Symbol c tv r
t)


--------------------------------------------------------------------------------
-- foldReft :: (Reftable r, TyConable c) => (r -> a -> a) -> a -> RType c tv r -> a
--------------------------------------------------------------------------------
-- foldReft f = efoldReft (\_ _ -> []) (\_ -> ()) (\_ _ -> f) (\_ γ -> γ) emptyF.SEnv

--------------------------------------------------------------------------------
foldReft :: (Reftable r, TyConable c) => BScope -> (F.SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a
--------------------------------------------------------------------------------
foldReft :: forall r c tv a.
(Reftable r, TyConable c) =>
Bool
-> (SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a
foldReft Bool
bsc SEnv (RType c tv r) -> r -> a -> a
f = (Symbol -> RType c tv r -> Bool)
-> Bool
-> (RType c tv r -> RType c tv r)
-> (SEnv (RType c tv r) -> Maybe (RType c tv r) -> r -> a -> a)
-> a
-> RType c tv r
-> a
forall r c tv b a.
(Reftable r, TyConable c) =>
(Symbol -> RType c tv r -> Bool)
-> Bool
-> (RType c tv r -> b)
-> (SEnv b -> Maybe (RType c tv r) -> r -> a -> a)
-> a
-> RType c tv r
-> a
foldReft'  (\Symbol
_ RType c tv r
_ -> Bool
False) Bool
bsc RType c tv r -> RType c tv r
forall a. a -> a
id (\SEnv (RType c tv r)
γ Maybe (RType c tv r)
_ -> SEnv (RType c tv r) -> r -> a -> a
f SEnv (RType c tv r)
γ)

--------------------------------------------------------------------------------
foldReft' :: (Reftable r, TyConable c)
          => (Symbol -> RType c tv r -> Bool)
          -> BScope
          -> (RType c tv r -> b)
          -> (F.SEnv b -> Maybe (RType c tv r) -> r -> a -> a)
          -> a -> RType c tv r -> a
--------------------------------------------------------------------------------
foldReft' :: forall r c tv b a.
(Reftable r, TyConable c) =>
(Symbol -> RType c tv r -> Bool)
-> Bool
-> (RType c tv r -> b)
-> (SEnv b -> Maybe (RType c tv r) -> r -> a -> a)
-> a
-> RType c tv r
-> a
foldReft' Symbol -> RType c tv r -> Bool
logicBind Bool
bsc RType c tv r -> b
g SEnv b -> Maybe (RType c tv r) -> r -> a -> a
f
  = (Symbol -> RType c tv r -> Bool)
-> Bool
-> (c -> [RType c tv r] -> [(Symbol, b)])
-> (RTVar tv (RType c tv ()) -> [(Symbol, b)])
-> (RType c tv r -> b)
-> (SEnv b -> Maybe (RType c tv r) -> r -> a -> a)
-> (PVar (RType c tv ()) -> SEnv b -> SEnv b)
-> SEnv b
-> a
-> RType c tv r
-> a
forall r c tv a b.
(Reftable r, TyConable c) =>
(Symbol -> RType c tv r -> Bool)
-> Bool
-> (c -> [RType c tv r] -> [(Symbol, a)])
-> (RTVar tv (RType c tv ()) -> [(Symbol, a)])
-> (RType c tv r -> a)
-> (SEnv a -> Maybe (RType c tv r) -> r -> b -> b)
-> (PVar (RType c tv ()) -> SEnv a -> SEnv a)
-> SEnv a
-> b
-> RType c tv r
-> b
efoldReft Symbol -> RType c tv r -> Bool
logicBind Bool
bsc
              (\c
_ [RType c tv r]
_ -> [])
              ([(Symbol, b)] -> RTVar tv (RType c tv ()) -> [(Symbol, b)]
forall a b. a -> b -> a
const [])
              RType c tv r -> b
g
              (\SEnv b
γ Maybe (RType c tv r)
t r
r a
z -> SEnv b -> Maybe (RType c tv r) -> r -> a -> a
f SEnv b
γ Maybe (RType c tv r)
t r
r a
z)
              (\PVar (RType c tv ())
_ SEnv b
γ -> SEnv b
γ)
              SEnv b
forall a. SEnv 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 :: Reftable r =>(p -> [RType c tv r] -> [(Symbol, a)])-> (RType c tv r -> a)-> (SEnv a -> Maybe (RType c tv r) -> r -> c1 -> c1)-> SEnv a-> c1-> RType c tv r-> c1
efoldReft :: (Reftable r, TyConable c)
          => (Symbol -> RType c tv r -> Bool)
          -> BScope
          -> (c  -> [RType c tv r] -> [(Symbol, a)])
          -> (RTVar tv (RType c tv ()) -> [(Symbol, a)])
          -> (RType c tv r -> a)
          -> (F.SEnv a -> Maybe (RType c tv r) -> r -> b -> b)
          -> (PVar (RType c tv ()) -> F.SEnv a -> F.SEnv a)
          -> F.SEnv a
          -> b
          -> RType c tv r
          -> b
efoldReft :: forall r c tv a b.
(Reftable r, TyConable c) =>
(Symbol -> RType c tv r -> Bool)
-> Bool
-> (c -> [RType c tv r] -> [(Symbol, a)])
-> (RTVar tv (RType c tv ()) -> [(Symbol, a)])
-> (RType c tv r -> a)
-> (SEnv a -> Maybe (RType c tv r) -> r -> b -> b)
-> (PVar (RType c tv ()) -> SEnv a -> SEnv a)
-> SEnv a
-> b
-> RType c tv r
-> b
efoldReft Symbol -> RType c tv r -> Bool
logicBind Bool
bsc c -> [RType c tv r] -> [(Symbol, a)]
cb RTVar tv (RType c tv ()) -> [(Symbol, a)]
dty RType c tv r -> a
g SEnv a -> Maybe (RType c tv r) -> r -> b -> b
f PVar (RType c tv ()) -> SEnv a -> SEnv a
fp = SEnv a -> b -> RType c tv r -> b
go
  where
    -- folding over RType
    go :: SEnv a -> b -> RType c tv r -> b
go SEnv a
γ b
z me :: RType c tv r
me@(RVar tv
_ r
r)                = SEnv a -> Maybe (RType c tv r) -> r -> b -> b
f SEnv a
γ (RType c tv r -> Maybe (RType c tv r)
forall a. a -> Maybe a
Just RType c tv r
me) r
r b
z
    go SEnv a
γ b
z me :: RType c tv r
me@(RAllT RTVar tv (RType c tv ())
a RType c tv r
t r
r)
       | RTVar tv (RType c tv ()) -> Bool
forall tv s. RTVar tv s -> Bool
tyVarIsVal RTVar tv (RType c tv ())
a                   = SEnv a -> Maybe (RType c tv r) -> r -> b -> b
f SEnv a
γ (RType c tv r -> Maybe (RType c tv r)
forall a. a -> Maybe a
Just RType c tv r
me) r
r (SEnv a -> b -> RType c tv r -> b
go (SEnv a -> [(Symbol, a)] -> SEnv a
forall a. SEnv a -> [(Symbol, a)] -> SEnv a
insertsSEnv SEnv a
γ (RTVar tv (RType c tv ()) -> [(Symbol, a)]
dty RTVar tv (RType c tv ())
a)) b
z RType c tv r
t)
       | Bool
otherwise                      = SEnv a -> Maybe (RType c tv r) -> r -> b -> b
f SEnv a
γ (RType c tv r -> Maybe (RType c tv r)
forall a. a -> Maybe a
Just RType c tv r
me) r
r (SEnv a -> b -> RType c tv r -> b
go SEnv a
γ b
z RType c tv r
t)
    go SEnv a
γ b
z (RAllP PVar (RType c tv ())
p RType c tv r
t)                  = SEnv a -> b -> RType c tv r -> b
go (PVar (RType c tv ()) -> SEnv a -> SEnv a
fp PVar (RType c tv ())
p SEnv a
γ) b
z RType c tv r
t
    go SEnv a
γ b
z me :: RType c tv r
me@(RFun Symbol
_ RFInfo{permitTC :: RFInfo -> Maybe Bool
permitTC = Maybe Bool
permitTC} (RApp c
c [RType c tv r]
ts [RTPropV Symbol c tv r]
_ r
_) RType 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  = SEnv a -> Maybe (RType c tv r) -> r -> b -> b
f SEnv a
γ (RType c tv r -> Maybe (RType c tv r)
forall a. a -> Maybe a
Just RType c tv r
me) r
r (SEnv a -> b -> RType c tv r -> b
go (SEnv a -> [(Symbol, a)] -> SEnv a
forall a. SEnv a -> [(Symbol, a)] -> SEnv a
insertsSEnv SEnv a
γ (c -> [RType c tv r] -> [(Symbol, a)]
cb c
c [RType c tv r]
ts)) (SEnv a -> b -> [RType c tv r] -> b
go' SEnv a
γ b
z [RType c tv r]
ts) RType c tv r
t')
    go SEnv a
γ b
z me :: RType c tv r
me@(RFun Symbol
x RFInfo
_ RType c tv r
t RType c tv r
t' r
r)
       | Symbol -> RType c tv r -> Bool
logicBind Symbol
x RType c tv r
t                  = SEnv a -> Maybe (RType c tv r) -> r -> b -> b
f SEnv a
γ (RType c tv r -> Maybe (RType c tv r)
forall a. a -> Maybe a
Just RType c tv r
me) r
r (SEnv a -> b -> RType c tv r -> b
go SEnv a
γ' (SEnv a -> b -> RType c tv r -> b
go SEnv a
γ b
z RType c tv r
t) RType c tv r
t')
       | Bool
otherwise                      = SEnv a -> Maybe (RType c tv r) -> r -> b -> b
f SEnv a
γ (RType c tv r -> Maybe (RType c tv r)
forall a. a -> Maybe a
Just RType c tv r
me) r
r (SEnv a -> b -> RType c tv r -> b
go SEnv a
γ  (SEnv a -> b -> RType c tv r -> b
go SEnv a
γ b
z RType c tv r
t) RType c tv r
t')
       where
         γ' :: SEnv a
γ'                             = Symbol -> a -> SEnv a -> SEnv a
forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv Symbol
x (RType c tv r -> a
g RType c tv r
t) SEnv a
γ
    go SEnv a
γ b
z me :: RType c tv r
me@(RApp c
_ [RType c tv r]
ts [RTPropV Symbol c tv r]
rs r
r)          = SEnv a -> Maybe (RType c tv r) -> r -> b -> b
f SEnv a
γ (RType c tv r -> Maybe (RType c tv r)
forall a. a -> Maybe a
Just RType c tv r
me) r
r (SEnv a -> b -> [RTPropV Symbol c tv r] -> b
ho' SEnv a
γ (SEnv a -> b -> [RType c tv r] -> b
go' SEnv a
γ' b
z [RType c tv r]
ts) [RTPropV Symbol c tv r]
rs)
       where γ' :: SEnv a
γ' = if Bool
bsc then Symbol -> a -> SEnv a -> SEnv a
forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv (RType c tv r -> Symbol
forall r c tv. Reftable r => RType c tv r -> Symbol
rTypeValueVar RType c tv r
me) (RType c tv r -> a
g RType c tv r
me) SEnv a
γ else SEnv a
γ

    go SEnv a
γ b
z (RAllE Symbol
x RType c tv r
t RType c tv r
t')               = SEnv a -> b -> RType c tv r -> b
go (Symbol -> a -> SEnv a -> SEnv a
forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv Symbol
x (RType c tv r -> a
g RType c tv r
t) SEnv a
γ) (SEnv a -> b -> RType c tv r -> b
go SEnv a
γ b
z RType c tv r
t) RType c tv r
t'
    go SEnv a
γ b
z (REx Symbol
x RType c tv r
t RType c tv r
t')                 = SEnv a -> b -> RType c tv r -> b
go (Symbol -> a -> SEnv a -> SEnv a
forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv Symbol
x (RType c tv r -> a
g RType c tv r
t) SEnv a
γ) (SEnv a -> b -> RType c tv r -> b
go SEnv a
γ b
z RType c tv r
t) RType c tv r
t'
    go SEnv a
γ b
z me :: RType c tv r
me@(RRTy [] r
r Oblig
_ RType c tv r
t)           = SEnv a -> Maybe (RType c tv r) -> r -> b -> b
f SEnv a
γ (RType c tv r -> Maybe (RType c tv r)
forall a. a -> Maybe a
Just RType c tv r
me) r
r (SEnv a -> b -> RType c tv r -> b
go SEnv a
γ b
z RType c tv r
t)
    go SEnv a
γ b
z me :: RType c tv r
me@(RRTy [(Symbol, RType c tv r)]
xts r
r Oblig
_ RType c tv r
t)          = SEnv a -> Maybe (RType c tv r) -> r -> b -> b
f SEnv a
γ (RType c tv r -> Maybe (RType c tv r)
forall a. a -> Maybe a
Just RType c tv r
me) r
r (SEnv a -> b -> RType c tv r -> b
go SEnv a
γ (SEnv a -> b -> RType c tv r -> b
go SEnv a
γ b
z ([(Symbol, RType c tv r)] -> RType c tv r
forall {r} {v} {c} {tv}.
Monoid r =>
[(Symbol, RTypeV v c tv r)] -> RTypeV v c tv r
envtoType [(Symbol, RType c tv r)]
xts)) RType c tv r
t)
    go SEnv a
γ b
z me :: RType c tv r
me@(RAppTy RType c tv r
t RType c tv r
t' r
r)           = SEnv a -> Maybe (RType c tv r) -> r -> b -> b
f SEnv a
γ (RType c tv r -> Maybe (RType c tv r)
forall a. a -> Maybe a
Just RType c tv r
me) r
r (SEnv a -> b -> RType c tv r -> b
go SEnv a
γ (SEnv a -> b -> RType c tv r -> b
go SEnv a
γ b
z RType c tv r
t) RType c tv r
t')
    go SEnv a
_ b
z (RExprArg Located (ExprV Symbol)
_)                 = b
z
    go SEnv a
γ b
z me :: RType c tv r
me@(RHole r
r)                 = SEnv a -> Maybe (RType c tv r) -> r -> b -> b
f SEnv a
γ (RType c tv r -> Maybe (RType c tv r)
forall a. a -> Maybe a
Just RType c tv r
me) r
r b
z

    -- folding over Ref
    ho :: SEnv a -> b -> RTPropV Symbol c tv r -> b
ho  SEnv a
γ b
z (RProp [(Symbol, RType c tv ())]
ss (RHole r
r))       = SEnv a -> Maybe (RType c tv r) -> r -> b -> b
f (SEnv a -> [(Symbol, a)] -> SEnv a
forall a. SEnv a -> [(Symbol, a)] -> SEnv a
insertsSEnv SEnv a
γ ((RType c tv () -> a) -> (Symbol, RType c tv ()) -> (Symbol, a)
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 -> a
g (RType c tv r -> a)
-> (RType c tv () -> RType c tv r) -> RType c tv () -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType c tv () -> RType c tv r
forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort) ((Symbol, RType c tv ()) -> (Symbol, a))
-> [(Symbol, RType c tv ())] -> [(Symbol, a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv ())]
ss)) Maybe (RType c tv r)
forall a. Maybe a
Nothing r
r b
z
    ho  SEnv a
γ b
z (RProp [(Symbol, RType c tv ())]
ss RType c tv r
t)               = SEnv a -> b -> RType c tv r -> b
go (SEnv a -> [(Symbol, a)] -> SEnv a
forall a. SEnv a -> [(Symbol, a)] -> SEnv a
insertsSEnv SEnv a
γ ((RType c tv () -> a) -> (Symbol, RType c tv ()) -> (Symbol, a)
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 -> a
g (RType c tv r -> a)
-> (RType c tv () -> RType c tv r) -> RType c tv () -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType c tv () -> RType c tv r
forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort) ((Symbol, RType c tv ()) -> (Symbol, a))
-> [(Symbol, RType c tv ())] -> [(Symbol, a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType c tv ())]
ss)) b
z RType c tv r
t

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

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

    envtoType :: [(Symbol, RTypeV v c tv r)] -> RTypeV v c tv r
envtoType [(Symbol, RTypeV v c tv r)]
xts = ((Symbol, RTypeV v c tv r) -> RTypeV v c tv r -> RTypeV v c tv r)
-> RTypeV v c tv r
-> [(Symbol, RTypeV v c tv r)]
-> RTypeV 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 (\(Symbol
x,RTypeV v c tv r
t1) RTypeV v c tv r
t2 -> Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
forall r v c tv.
Monoid r =>
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
rFun Symbol
x RTypeV v c tv r
t1 RTypeV v c tv r
t2) ((Symbol, RTypeV v c tv r) -> RTypeV v c tv r
forall a b. (a, b) -> b
snd ((Symbol, RTypeV v c tv r) -> RTypeV v c tv r)
-> (Symbol, RTypeV v c tv r) -> RTypeV v c tv r
forall a b. (a -> b) -> a -> b
$ [(Symbol, RTypeV v c tv r)] -> (Symbol, RTypeV v c tv r)
forall a. HasCallStack => [a] -> a
last [(Symbol, RTypeV v c tv r)]
xts) ([(Symbol, RTypeV v c tv r)] -> [(Symbol, RTypeV v c tv r)]
forall a. HasCallStack => [a] -> [a]
init [(Symbol, RTypeV 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 RTVUV Symbol c tv
α RTypeV Symbol c tv r
t r
r)     = RTVUV Symbol c tv
-> RTypeV Symbol c tv r -> r -> RTypeV Symbol c tv r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV Symbol c tv
α ((RFInfo -> RFInfo) -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeV Symbol c tv r
t) r
r
mapRFInfo RFInfo -> RFInfo
f (RAllP PVUV Symbol c tv
π RTypeV Symbol c tv r
t)       = PVUV Symbol c tv -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV Symbol c tv
π ((RFInfo -> RFInfo) -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeV Symbol c tv r
t)
mapRFInfo RFInfo -> RFInfo
f (RFun Symbol
x RFInfo
i RTypeV Symbol c tv r
t RTypeV Symbol c tv r
t' r
r) = Symbol
-> RFInfo
-> RTypeV Symbol c tv r
-> RTypeV Symbol c tv r
-> r
-> RTypeV Symbol c tv r
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
x (RFInfo -> RFInfo
f RFInfo
i) ((RFInfo -> RFInfo) -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeV Symbol c tv r
t) ((RFInfo -> RFInfo) -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeV Symbol c tv r
t') r
r
mapRFInfo RFInfo -> RFInfo
f (RAppTy RTypeV Symbol c tv r
t RTypeV Symbol c tv r
t' r
r)   = RTypeV Symbol c tv r
-> RTypeV Symbol c tv r -> r -> RTypeV Symbol c tv r
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy ((RFInfo -> RFInfo) -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeV Symbol c tv r
t) ((RFInfo -> RFInfo) -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeV Symbol c tv r
t') r
r
mapRFInfo RFInfo -> RFInfo
f (RApp c
c [RTypeV Symbol c tv r]
ts [RTPropV Symbol c tv r]
rs r
r)  = c
-> [RTypeV Symbol c tv r]
-> [RTPropV Symbol c tv r]
-> r
-> RTypeV Symbol c tv r
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp c
c ((RFInfo -> RFInfo) -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f (RTypeV Symbol c tv r -> RTypeV Symbol c tv r)
-> [RTypeV Symbol c tv r] -> [RTypeV Symbol c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeV Symbol c tv r]
ts) ((RFInfo -> RFInfo)
-> RTPropV Symbol c tv r -> RTPropV Symbol c tv r
forall τ c tv r.
(RFInfo -> RFInfo) -> Ref τ (RType c tv r) -> Ref τ (RType c tv r)
mapRFInfoRef RFInfo -> RFInfo
f (RTPropV Symbol c tv r -> RTPropV Symbol c tv r)
-> [RTPropV Symbol c tv r] -> [RTPropV Symbol c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropV Symbol c tv r]
rs) r
r
mapRFInfo RFInfo -> RFInfo
f (REx Symbol
b RTypeV Symbol c tv r
t1 RTypeV Symbol c tv r
t2)     = Symbol
-> RTypeV Symbol c tv r
-> RTypeV Symbol c tv r
-> RTypeV Symbol c tv r
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
REx Symbol
b  ((RFInfo -> RFInfo) -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeV Symbol c tv r
t1) ((RFInfo -> RFInfo) -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeV Symbol c tv r
t2)
mapRFInfo RFInfo -> RFInfo
f (RAllE Symbol
b RTypeV Symbol c tv r
t1 RTypeV Symbol c tv r
t2)   = Symbol
-> RTypeV Symbol c tv r
-> RTypeV Symbol c tv r
-> RTypeV Symbol c tv r
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
RAllE Symbol
b ((RFInfo -> RFInfo) -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeV Symbol c tv r
t1) ((RFInfo -> RFInfo) -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeV Symbol c tv r
t2)
mapRFInfo RFInfo -> RFInfo
f (RRTy [(Symbol, RTypeV Symbol c tv r)]
e r
r Oblig
o RTypeV Symbol c tv r
t)    = [(Symbol, RTypeV Symbol c tv r)]
-> r -> Oblig -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy ((RTypeV Symbol c tv r -> RTypeV Symbol c tv r)
-> (Symbol, RTypeV Symbol c tv r) -> (Symbol, RTypeV 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) -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f) ((Symbol, RTypeV Symbol c tv r) -> (Symbol, RTypeV Symbol c tv r))
-> [(Symbol, RTypeV Symbol c tv r)]
-> [(Symbol, RTypeV Symbol c tv r)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RTypeV Symbol c tv r)]
e) r
r Oblig
o ((RFInfo -> RFInfo) -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall c tv r. (RFInfo -> RFInfo) -> RType c tv r -> RType c tv r
mapRFInfo RFInfo -> RFInfo
f RTypeV Symbol c tv r
t)
mapRFInfo RFInfo -> RFInfo
_ RTypeV Symbol c tv r
t'                = RTypeV 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 -> Ref τ (RType c tv r)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, τ)]
s (RType c tv r -> Ref τ (RType c tv r))
-> RType c tv r -> Ref τ (RType c tv r)
forall a b. (a -> b) -> a -> b
$ r -> RType c tv r
forall v c tv r. r -> RTypeV v c tv r
RHole r
r
mapRFInfoRef RFInfo -> RFInfo
f (RProp [(Symbol, τ)]
s RType c tv r
t)    = [(Symbol, τ)] -> RType c tv r -> Ref τ (RType c tv r)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp  [(Symbol, τ)]
s (RType c tv r -> Ref τ (RType c tv r))
-> RType c tv r -> Ref τ (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 RTVUV Symbol c tv
α RType c tv r
t r
r)     = RTVUV Symbol c tv -> RType c tv r -> r -> RType c tv r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV 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 PVUV Symbol c tv
π RType c tv r
t)       = PVUV Symbol c tv -> RType c tv r -> RType c tv r
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV 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 v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV 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 v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV 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 [RTPropV 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] -> [RTPropV Symbol c tv r] -> r -> RType c tv r
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV 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)
-> RTPropV Symbol c tv r -> RTPropV 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 (RTPropV Symbol c tv r -> RTPropV Symbol c tv r)
-> [RTPropV Symbol c tv r] -> [RTPropV Symbol c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropV 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 v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV 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 v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV 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 v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV 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 -> Ref τ (RType c tv r)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, τ)]
s (RType c tv r -> Ref τ (RType c tv r))
-> RType c tv r -> Ref τ (RType c tv r)
forall a b. (a -> b) -> a -> b
$ r -> RType c tv r
forall v c tv r. r -> RTypeV 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 -> Ref τ (RType c tv r)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, τ)]
s (RType c tv r -> Ref τ (RType c tv r))
-> RType c tv r -> Ref τ (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 :: (Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
mapBind :: forall v c tv r.
(Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
mapBind Symbol -> Symbol
f (RAllT RTVUV v c tv
α RTypeV v c tv r
t r
r)      = RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV v c tv
α ((Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r.
(Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
mapBind Symbol -> Symbol
f RTypeV v c tv r
t) r
r
mapBind Symbol -> Symbol
f (RAllP PVUV v c tv
π RTypeV v c tv r
t)        = PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV v c tv
π ((Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r.
(Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
mapBind Symbol -> Symbol
f RTypeV v c tv r
t)
mapBind Symbol -> Symbol
f (RFun Symbol
b RFInfo
i RTypeV v c tv r
t1 RTypeV v c tv r
t2 r
r) = Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun (Symbol -> Symbol
f Symbol
b) RFInfo
i ((Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r.
(Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
mapBind Symbol -> Symbol
f RTypeV v c tv r
t1) ((Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r.
(Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
mapBind Symbol -> Symbol
f RTypeV v c tv r
t2) r
r
mapBind Symbol -> Symbol
f (RApp c
c [RTypeV v c tv r]
ts [RTPropV v c tv r]
rs r
r)   = c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp c
c ((Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r.
(Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
mapBind Symbol -> Symbol
f (RTypeV v c tv r -> RTypeV v c tv r)
-> [RTypeV v c tv r] -> [RTypeV v c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeV v c tv r]
ts) ((Symbol -> Symbol) -> RTPropV v c tv r -> RTPropV v c tv r
forall τ v c tv r.
(Symbol -> Symbol)
-> Ref τ (RTypeV v c tv r) -> Ref τ (RTypeV v c tv r)
mapBindRef Symbol -> Symbol
f (RTPropV v c tv r -> RTPropV v c tv r)
-> [RTPropV v c tv r] -> [RTPropV v c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropV v c tv r]
rs) r
r
mapBind Symbol -> Symbol
f (RAllE Symbol
b RTypeV v c tv r
t1 RTypeV v c tv r
t2)    = Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
RAllE  (Symbol -> Symbol
f Symbol
b) ((Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r.
(Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
mapBind Symbol -> Symbol
f RTypeV v c tv r
t1) ((Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r.
(Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
mapBind Symbol -> Symbol
f RTypeV v c tv r
t2)
mapBind Symbol -> Symbol
f (REx Symbol
b RTypeV v c tv r
t1 RTypeV v c tv r
t2)      = Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
REx    (Symbol -> Symbol
f Symbol
b) ((Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r.
(Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
mapBind Symbol -> Symbol
f RTypeV v c tv r
t1) ((Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r.
(Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
mapBind Symbol -> Symbol
f RTypeV v c tv r
t2)
mapBind Symbol -> Symbol
_ (RVar tv
α r
r)         = tv -> r -> RTypeV v c tv r
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar tv
α r
r
mapBind Symbol -> Symbol
_ (RHole r
r)          = r -> RTypeV v c tv r
forall v c tv r. r -> RTypeV v c tv r
RHole r
r
mapBind Symbol -> Symbol
f (RRTy [(Symbol, RTypeV v c tv r)]
e r
r Oblig
o RTypeV v c tv r
t)     = [(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v c tv r
RRTy [(Symbol, RTypeV v c tv r)]
e r
r Oblig
o ((Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r.
(Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
mapBind Symbol -> Symbol
f RTypeV v c tv r
t)
mapBind Symbol -> Symbol
_ (RExprArg Located (ExprV v)
e)       = Located (ExprV v) -> RTypeV v c tv r
forall v c tv r. Located (ExprV v) -> RTypeV v c tv r
RExprArg Located (ExprV v)
e
mapBind Symbol -> Symbol
f (RAppTy RTypeV v c tv r
t RTypeV v c tv r
t' r
r)    = RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy ((Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r.
(Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
mapBind Symbol -> Symbol
f RTypeV v c tv r
t) ((Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r.
(Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
mapBind Symbol -> Symbol
f RTypeV v c tv r
t') r
r

mapBindRef :: (Symbol -> Symbol)
           -> Ref τ (RTypeV v c tv r) -> Ref τ (RTypeV v c tv r)
mapBindRef :: forall τ v c tv r.
(Symbol -> Symbol)
-> Ref τ (RTypeV v c tv r) -> Ref τ (RTypeV v c tv r)
mapBindRef Symbol -> Symbol
f (RProp [(Symbol, τ)]
s (RHole r
r)) = [(Symbol, τ)] -> RTypeV v c tv r -> Ref τ (RTypeV v c tv r)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp ((Symbol -> Symbol) -> (Symbol, τ) -> (Symbol, τ)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Symbol -> Symbol
f ((Symbol, τ) -> (Symbol, τ)) -> [(Symbol, τ)] -> [(Symbol, τ)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, τ)]
s) (r -> RTypeV v c tv r
forall v c tv r. r -> RTypeV v c tv r
RHole r
r)
mapBindRef Symbol -> Symbol
f (RProp [(Symbol, τ)]
s RTypeV v c tv r
t)         = [(Symbol, τ)] -> RTypeV v c tv r -> Ref τ (RTypeV v c tv r)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp ((Symbol -> Symbol) -> (Symbol, τ) -> (Symbol, τ)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Symbol -> Symbol
f ((Symbol, τ) -> (Symbol, τ)) -> [(Symbol, τ)] -> [(Symbol, τ)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, τ)]
s) (RTypeV v c tv r -> Ref τ (RTypeV v c tv r))
-> RTypeV v c tv r -> Ref τ (RTypeV v c tv r)
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r.
(Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
mapBind Symbol -> Symbol
f RTypeV v c tv r
t


--------------------------------------------------
ofRSort ::  Reftable r => RType c tv () -> RType c tv r
ofRSort :: forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort = (() -> r) -> RTypeV Symbol c tv () -> RTypeV Symbol c tv r
forall a b.
(a -> b) -> RTypeV Symbol c tv a -> RTypeV Symbol c tv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap () -> r
forall a. Monoid a => a
mempty

toRSort :: RTypeV v c tv r -> RTypeV v c tv ()
toRSort :: forall v c tv r. RTypeV v c tv r -> RTypeV v c tv ()
toRSort = RTypeV v c tv () -> RTypeV v c tv ()
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv r
stripAnnotations (RTypeV v c tv () -> RTypeV v c tv ())
-> (RTypeV v c tv r -> RTypeV v c tv ())
-> RTypeV v c tv r
-> RTypeV v c tv ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Symbol) -> RTypeV v c tv () -> RTypeV v c tv ()
forall v c tv r.
(Symbol -> Symbol) -> RTypeV v c tv r -> RTypeV v c tv r
mapBind (Symbol -> Symbol -> Symbol
forall a b. a -> b -> a
const Symbol
F.dummySymbol) (RTypeV v c tv () -> RTypeV v c tv ())
-> (RTypeV v c tv r -> RTypeV v c tv ())
-> RTypeV v c tv r
-> RTypeV v c tv ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeV v c tv r -> RTypeV v c tv ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void

stripAnnotations :: RTypeV v c tv r -> RTypeV v c tv r
stripAnnotations :: forall v c tv r. RTypeV v c tv r -> RTypeV v c tv r
stripAnnotations (RAllT RTVUV v c tv
α RTypeV v c tv r
t r
r)     = RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV v c tv
α (RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv r
stripAnnotations RTypeV v c tv r
t) r
r
stripAnnotations (RAllP PVUV v c tv
_ RTypeV v c tv r
t)       = RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv r
stripAnnotations RTypeV v c tv r
t
stripAnnotations (RAllE Symbol
_ RTypeV v c tv r
_ RTypeV v c tv r
t)     = RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv r
stripAnnotations RTypeV v c tv r
t
stripAnnotations (REx Symbol
_ RTypeV v c tv r
_ RTypeV v c tv r
t)       = RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv r
stripAnnotations RTypeV v c tv r
t
stripAnnotations (RFun Symbol
x RFInfo
i RTypeV v c tv r
t RTypeV v c tv r
t' r
r) = Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v c tv r
RFun Symbol
x RFInfo
i (RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv r
stripAnnotations RTypeV v c tv r
t) (RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv r
stripAnnotations RTypeV v c tv r
t') r
r
stripAnnotations (RAppTy RTypeV v c tv r
t RTypeV v c tv r
t' r
r)   = RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
forall v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAppTy (RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv r
stripAnnotations RTypeV v c tv r
t) (RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv r
stripAnnotations RTypeV v c tv r
t') r
r
stripAnnotations (RApp c
c [RTypeV v c tv r]
ts [RTPropV v c tv r]
rs r
r)  = c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp c
c (RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv r
stripAnnotations (RTypeV v c tv r -> RTypeV v c tv r)
-> [RTypeV v c tv r] -> [RTypeV v c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTypeV v c tv r]
ts) (RTPropV v c tv r -> RTPropV v c tv r
forall τ v c tv r.
Ref τ (RTypeV v c tv r) -> Ref τ (RTypeV v c tv r)
stripAnnotationsRef (RTPropV v c tv r -> RTPropV v c tv r)
-> [RTPropV v c tv r] -> [RTPropV v c tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropV v c tv r]
rs) r
r
stripAnnotations (RRTy [(Symbol, RTypeV v c tv r)]
_ r
_ Oblig
_ RTypeV v c tv r
t)    = RTypeV v c tv r -> RTypeV v c tv r
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv r
stripAnnotations RTypeV v c tv r
t
stripAnnotations RTypeV v c tv r
t                 = RTypeV v c tv r
t

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

insertSEnv :: F.Symbol -> a -> F.SEnv a -> F.SEnv a
insertSEnv :: forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv = Symbol -> a -> SEnv a -> SEnv a
forall a. Symbol -> a -> SEnv a -> SEnv a
F.insertSEnv

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

rTypeValueVar :: (Reftable r) => RType c tv r -> Symbol
rTypeValueVar :: forall r c tv. Reftable r => RType c tv r -> Symbol
rTypeValueVar RType c tv r
t = Symbol
vv where F.Reft (Symbol
vv,ExprV Symbol
_) =  RType c tv r -> ReftV Symbol
forall r c tv. Reftable r => RType c tv r -> ReftV Symbol
rTypeReft RType c tv r
t

rTypeReft :: (Reftable r) => RType c tv r -> F.Reft
rTypeReft :: forall r c tv. Reftable r => RType c tv r -> ReftV Symbol
rTypeReft = ReftV Symbol -> (r -> ReftV Symbol) -> Maybe r -> ReftV Symbol
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ReftV Symbol
forall v. ReftV v
F.trueReft r -> ReftV Symbol
forall r. Reftable r => r -> ReftV Symbol
toReft (Maybe r -> ReftV Symbol)
-> (RType c tv r -> Maybe r) -> RType c tv r -> ReftV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType c tv r -> Maybe r
forall c tv r. RType c tv r -> Maybe r
stripRTypeBase

-- stripRTypeBase ::  RType a -> Maybe a
stripRTypeBase :: RType c tv r -> Maybe r
stripRTypeBase :: forall c tv r. RType c tv r -> Maybe r
stripRTypeBase (RApp c
_ [RTypeV Symbol c tv r]
_ [RTPropV Symbol 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 Symbol
_ RFInfo
_ RTypeV Symbol c tv r
_ RTypeV Symbol c tv r
_ r
x) = r -> Maybe r
forall a. a -> Maybe a
Just r
x
stripRTypeBase (RAppTy RTypeV Symbol c tv r
_ RTypeV Symbol c tv r
_ r
x)   = r -> Maybe r
forall a. a -> Maybe a
Just r
x
stripRTypeBase (RAllT RTVUV Symbol c tv
_ RTypeV Symbol c tv r
_ r
x)    = r -> Maybe r
forall a. a -> Maybe a
Just r
x
stripRTypeBase RTypeV Symbol c tv r
_                = Maybe r
forall a. Maybe a
Nothing

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