{-# Language ImplicitParams #-}
{-# Language FlexibleInstances #-}
{-# Language RecursiveDo #-}
{-# Language BlockArguments #-}
{-# Language RankNTypes #-}
{-# Language OverloadedStrings #-}
module Cryptol.TypeCheck.ModuleBacktickInstance
  ( MBQual
  , doBacktickInstance
  ) where

import Data.Set(Set)
import qualified Data.Set as Set
import Data.Map(Map)
import qualified Data.Map as Map
import MonadLib
import Data.List(group,sort)
import Data.Maybe(mapMaybe)
import qualified Data.Text as Text

import Cryptol.Utils.Ident(ModPath(..), modPathIsOrContains,Namespace(..)
                          , Ident, mkIdent, identText
                          , ModName, modNameChunksText )
import Cryptol.Utils.PP(pp)
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.RecordMap(RecordMap,recordFromFields,recordFromFieldsErr)
import Cryptol.Parser.Position
import Cryptol.ModuleSystem.Name(
  nameModPath, nameModPathMaybe, nameIdent, mapNameIdent)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Error
import qualified Cryptol.TypeCheck.Monad as TC


type MBQual a = (Maybe ModName, a)

{- | Rewrite declarations to add the given module parameters.
Assumes the renaming due to the instantiation has already happened.
The module being rewritten should not contain any nested functors
(or module with only top-level constraints) because it is not clear
how to parameterize the parameters.
-}
doBacktickInstance ::
  Set (MBQual TParam) ->
  [Prop] ->
  Map (MBQual Name) Type ->
  ModuleG (Located (ImpName Name)) ->
  TC.InferM (ModuleG (Located (ImpName Name)))
doBacktickInstance :: Set (MBQual TParam)
-> [Prop]
-> Map (MBQual Name) Prop
-> ModuleG (Located (ImpName Name))
-> InferM (ModuleG (Located (ImpName Name)))
doBacktickInstance Set (MBQual TParam)
as [Prop]
ps Map (MBQual Name) Prop
mp ModuleG (Located (ImpName Name))
m
  | forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set (MBQual TParam)
as Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Prop]
ps Bool -> Bool -> Bool
&& forall k a. Map k a -> Bool
Map.null Map (MBQual Name) Prop
mp = forall (f :: * -> *) a. Applicative f => a -> f a
pure ModuleG (Located (ImpName Name))
m
  | Bool
otherwise =
    forall i (m :: * -> *) a. i -> ReaderT i m a -> m a
runReaderT
      RO { isOurs :: Name -> Bool
isOurs = \Name
x -> case Name -> Maybe ModPath
nameModPathMaybe Name
x of
                            Maybe ModPath
Nothing -> Bool
False
                            Just ModPath
y  -> ModPath
ourPath ModPath -> ModPath -> Bool
`modPathIsOrContains` ModPath
y
         , tparams :: [MBQual TParam]
tparams = forall a. Set a -> [a]
Set.toList Set (MBQual TParam)
as
         , constraints :: [Prop]
constraints = [Prop]
ps
         , vparams :: Map (MBQual Name) Prop
vparams = Map (MBQual Name) Prop
mp
         , newNewtypes :: Map Name Newtype
newNewtypes = forall k a. Map k a
Map.empty
         }

    do forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(BIWhat, Name)]
bad)
              (Error -> RewM ()
recordError (BadBacktickInstance -> Error
FunctorInstanceBadBacktick ([(BIWhat, Name)] -> BadBacktickInstance
BINested [(BIWhat, Name)]
bad)))

       rec
         Map Name TySyn
ts <- forall {a}.
AddParams a =>
Map Name Newtype
-> (ModuleG (Located (ImpName Name)) -> a) -> ReaderT RO InferM a
doAddParams Map Name Newtype
nt forall mname. ModuleG mname -> Map Name TySyn
mTySyns
         Map Name Newtype
nt <- forall {a}.
AddParams a =>
Map Name Newtype
-> (ModuleG (Located (ImpName Name)) -> a) -> ReaderT RO InferM a
doAddParams Map Name Newtype
nt forall mname. ModuleG mname -> Map Name Newtype
mNewtypes
         [DeclGroup]
ds <- forall {a}.
AddParams a =>
Map Name Newtype
-> (ModuleG (Located (ImpName Name)) -> a) -> ReaderT RO InferM a
doAddParams Map Name Newtype
nt forall mname. ModuleG mname -> [DeclGroup]
mDecls

       forall (f :: * -> *) a. Applicative f => a -> f a
pure ModuleG (Located (ImpName Name))
m
         { mTySyns :: Map Name TySyn
mTySyns   = Map Name TySyn
ts
         , mNewtypes :: Map Name Newtype
mNewtypes = Map Name Newtype
nt
         , mDecls :: [DeclGroup]
mDecls    = [DeclGroup]
ds
         }

    where
    bad :: [(BIWhat, Name)]
bad = forall {b} {a} {a}.
(ModuleG (Located (ImpName Name)) -> Map b a) -> a -> [(a, b)]
mkBad forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors BIWhat
BIFunctor
       forall a. [a] -> [a] -> [a]
++ forall {b} {a} {a}.
(ModuleG (Located (ImpName Name)) -> Map b a) -> a -> [(a, b)]
mkBad forall mname. ModuleG mname -> Map Name AbstractType
mPrimTypes BIWhat
BIAbstractType
       forall a. [a] -> [a] -> [a]
++ forall {b} {a} {a}.
(ModuleG (Located (ImpName Name)) -> Map b a) -> a -> [(a, b)]
mkBad forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures BIWhat
BIInterface

    mkBad :: (ModuleG (Located (ImpName Name)) -> Map b a) -> a -> [(a, b)]
mkBad ModuleG (Located (ImpName Name)) -> Map b a
sel a
a = [ (a
a,b
k) | b
k <- forall k a. Map k a -> [k]
Map.keys (ModuleG (Located (ImpName Name)) -> Map b a
sel ModuleG (Located (ImpName Name))
m) ]

    ourPath :: ModPath
ourPath = case forall a. Located a -> a
thing (forall mname. ModuleG mname -> mname
mName ModuleG (Located (ImpName Name))
m) of
                ImpTop ModName
mo    -> ModName -> ModPath
TopModule ModName
mo
                ImpNested Name
mo -> ModPath -> Ident -> ModPath
Nested (Name -> ModPath
nameModPath Name
mo) (Name -> Ident
nameIdent Name
mo)

    doAddParams :: Map Name Newtype
-> (ModuleG (Located (ImpName Name)) -> a) -> ReaderT RO InferM a
doAddParams Map Name Newtype
nt ModuleG (Located (ImpName Name)) -> a
sel =
      forall (m :: * -> *) r a. RunReaderM m r => (r -> r) -> m a -> m a
mapReader (\RO
ro -> RO
ro { newNewtypes :: Map Name Newtype
newNewtypes = Map Name Newtype
nt }) (forall t. AddParams t => t -> RewM t
addParams (ModuleG (Located (ImpName Name)) -> a
sel ModuleG (Located (ImpName Name))
m))


type RewM = ReaderT RO TC.InferM

recordError :: Error -> RewM ()
recordError :: Error -> RewM ()
recordError Error
e = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift (Error -> InferM ()
TC.recordError Error
e)

data RO = RO
  { RO -> Name -> Bool
isOurs       :: Name -> Bool
  , RO -> [MBQual TParam]
tparams      :: [MBQual TParam]
  , RO -> [Prop]
constraints  :: [Prop]
  , RO -> Map (MBQual Name) Prop
vparams      :: Map (MBQual Name) Type
  , RO -> Map Name Newtype
newNewtypes  :: Map Name Newtype
  }


class AddParams t where
  addParams :: t -> RewM t

instance AddParams a => AddParams (Map Name a) where
  addParams :: Map Name a -> RewM (Map Name a)
addParams = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t. AddParams t => t -> RewM t
addParams

instance AddParams a => AddParams [a] where
  addParams :: [a] -> RewM [a]
addParams = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t. AddParams t => t -> RewM t
addParams

instance AddParams Newtype where
  addParams :: Newtype -> RewM Newtype
addParams Newtype
nt =
    do (TypeParams
tps,[Prop]
cs) <- (Name -> TPFlavor) -> RewM (TypeParams, [Prop])
newTypeParams Name -> TPFlavor
TPNewtypeParam
       [Prop]
rProps   <- forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (Newtype -> [Prop]
ntConstraints Newtype
nt)
       RecordMap Ident Prop
rFields  <- forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (Newtype -> RecordMap Ident Prop
ntFields Newtype
nt)
       forall (f :: * -> *) a. Applicative f => a -> f a
pure Newtype
nt
         { ntParams :: [TParam]
ntParams       = forall decl use. Params decl use -> [decl]
pDecl TypeParams
tps forall a. [a] -> [a] -> [a]
++ Newtype -> [TParam]
ntParams Newtype
nt
         , ntConstraints :: [Prop]
ntConstraints  = [Prop]
cs forall a. [a] -> [a] -> [a]
++ [Prop]
rProps
         , ntFields :: RecordMap Ident Prop
ntFields       = RecordMap Ident Prop
rFields
         }

instance AddParams TySyn where
  addParams :: TySyn -> RewM TySyn
addParams TySyn
ts =
    do (TypeParams
tps,[Prop]
cs) <- (Name -> TPFlavor) -> RewM (TypeParams, [Prop])
newTypeParams Name -> TPFlavor
TPTySynParam
       [Prop]
rProps   <- forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (TySyn -> [Prop]
tsConstraints TySyn
ts)
       Prop
rDef     <- forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (TySyn -> Prop
tsDef TySyn
ts)
       forall (f :: * -> *) a. Applicative f => a -> f a
pure TySyn
ts
         { tsParams :: [TParam]
tsParams      = forall decl use. Params decl use -> [decl]
pDecl TypeParams
tps forall a. [a] -> [a] -> [a]
++ TySyn -> [TParam]
tsParams TySyn
ts
         , tsConstraints :: [Prop]
tsConstraints = [Prop]
cs forall a. [a] -> [a] -> [a]
++ [Prop]
rProps
         , tsDef :: Prop
tsDef         = Prop
rDef
         }

instance AddParams DeclGroup where
  addParams :: DeclGroup -> RewM DeclGroup
addParams DeclGroup
dg =
    case DeclGroup
dg of
      Recursive [Decl]
ds   -> [Decl] -> DeclGroup
Recursive forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. AddParams t => t -> RewM t
addParams [Decl]
ds
      NonRecursive Decl
d -> Decl -> DeclGroup
NonRecursive forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. AddParams t => t -> RewM t
addParams Decl
d

instance AddParams Decl where
  addParams :: Decl -> RewM Decl
addParams Decl
d =
    case Decl -> DeclDef
dDefinition Decl
d of
      DeclDef
DPrim       -> BIWhat -> RewM Decl
bad BIWhat
BIPrimitive
      DForeign {} -> BIWhat -> RewM Decl
bad BIWhat
BIForeign
      DExpr Expr
e ->
        do (TypeParams
tps,[Prop]
cs) <- (Name -> TPFlavor) -> RewM (TypeParams, [Prop])
newTypeParams Name -> TPFlavor
TPSchemaParam
           (ValParams
vps,[(Name, Prop)]
bs) <- TypeParams -> RewM (ValParams, [(Name, Prop)])
newValParams TypeParams
tps
           let s :: Schema
s = Decl -> Schema
dSignature Decl
d

           Prop
ty1 <- forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (Schema -> Prop
sType Schema
s)
           [Prop]
ps1 <- forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (Schema -> [Prop]
sProps Schema
s)
           let ty2 :: Prop
ty2 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Prop -> Prop
tFun Prop
ty1 (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Name, Prop)]
bs)

           Expr
e1 <- forall t. RewVal t => TypeParams -> Int -> ValParams -> t -> RewM t
rewValM TypeParams
tps (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Prop]
cs) ValParams
vps Expr
e
           let ([TParam]
das,Expr
e2) = forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe (TParam, Expr)
splitTAbs     Expr
e1
               ([Prop]
dcs,Expr
e3) = forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe (Prop, Expr)
splitProofAbs Expr
e2
               e4 :: Expr
e4 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Prop -> Expr -> Expr
EAbs) Expr
e3 [(Name, Prop)]
bs
               e5 :: Expr
e5 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Expr -> Expr
EProofAbs Expr
e4 ([Prop]
cs forall a. [a] -> [a] -> [a]
++ [Prop]
dcs)
               e6 :: Expr
e6 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Expr -> Expr
ETAbs     Expr
e5 (forall decl use. Params decl use -> [decl]
pDecl TypeParams
tps forall a. [a] -> [a] -> [a]
++ [TParam]
das)

               s1 :: Schema
s1 = Forall
                      { sVars :: [TParam]
sVars  = forall decl use. Params decl use -> [decl]
pDecl TypeParams
tps forall a. [a] -> [a] -> [a]
++ Schema -> [TParam]
sVars Schema
s
                      , sProps :: [Prop]
sProps = [Prop]
cs forall a. [a] -> [a] -> [a]
++ [Prop]
ps1
                      , sType :: Prop
sType  = Prop
ty2
                      }

           forall (f :: * -> *) a. Applicative f => a -> f a
pure Decl
d { dDefinition :: DeclDef
dDefinition = Expr -> DeclDef
DExpr Expr
e6
                  , dSignature :: Schema
dSignature  = Schema
s1
                  }
    where
    bad :: BIWhat -> RewM Decl
bad BIWhat
w =
      do Error -> RewM ()
recordError (BadBacktickInstance -> Error
FunctorInstanceBadBacktick ([(BIWhat, Name)] -> BadBacktickInstance
BINested [(BIWhat
w,Decl -> Name
dName Decl
d)]))
         forall (f :: * -> *) a. Applicative f => a -> f a
pure Decl
d

data Params decl use = Params
  { forall decl use. Params decl use -> [decl]
pDecl   :: [decl]
  , forall decl use. Params decl use -> [use]
pUse    :: [use]
  , forall decl use. Params decl use -> Map decl use
pSubst  :: Map decl use
  }

noParams :: Params decl use
noParams :: forall decl use. Params decl use
noParams = Params
  { pDecl :: [decl]
pDecl   = []
  , pUse :: [use]
pUse    = []
  , pSubst :: Map decl use
pSubst  = forall k a. Map k a
Map.empty
  }

qualLabel :: Maybe ModName -> Ident -> Ident
qualLabel :: Maybe ModName -> Ident -> Ident
qualLabel Maybe ModName
mb Ident
i =
  case Maybe ModName
mb of
    Maybe ModName
Nothing -> Ident
i
    Just ModName
mn ->
      let txt :: Text
txt = Text -> [Text] -> Text
Text.intercalate Text
"'" (ModName -> [Text]
modNameChunksText ModName
mn forall a. [a] -> [a] -> [a]
++ [Ident -> Text
identText Ident
i])
      in Text -> Ident
mkIdent Text
txt


type TypeParams = Params TParam Type
type ValParams  = Params Name   Expr

newTypeParams :: (Name -> TPFlavor) -> RewM (TypeParams,[Prop])
newTypeParams :: (Name -> TPFlavor) -> RewM (TypeParams, [Prop])
newTypeParams Name -> TPFlavor
flav =
  do RO
ro <- forall (m :: * -> *) i. ReaderM m i => m i
ask
     let newFlaf :: Maybe ModName -> Name -> TPFlavor
newFlaf Maybe ModName
q = Name -> TPFlavor
flav forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ident -> Ident) -> Name -> Name
mapNameIdent (Maybe ModName -> Ident -> Ident
qualLabel Maybe ModName
q)
     [TParam]
as <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (RO -> [MBQual TParam]
tparams RO
ro) \(Maybe ModName
q,TParam
a) -> (Name -> TPFlavor) -> TParam -> InferM TParam
TC.freshTParam (Maybe ModName -> Name -> TPFlavor
newFlaf Maybe ModName
q) TParam
a)
     let bad :: [Ident]
bad = [ Ident
x
               | Ident
x : Ident
_ : [Ident]
_ <- forall a. Eq a => [a] -> [[a]]
group (forall a. Ord a => [a] -> [a]
sort (forall a b. (a -> b) -> [a] -> [b]
map Name -> Ident
nameIdent (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TParam -> Maybe Name
tpName [TParam]
as)))
               ]
     forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Ident]
bad \Ident
i ->
       Error -> RewM ()
recordError (BadBacktickInstance -> Error
FunctorInstanceBadBacktick (Ident -> BadBacktickInstance
BIMultipleParams Ident
i))

     let ts :: [Prop]
ts = forall a b. (a -> b) -> [a] -> [b]
map (TVar -> Prop
TVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> TVar
TVBound) [TParam]
as
         su :: Map TParam Prop
su = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd (RO -> [MBQual TParam]
tparams RO
ro)) [Prop]
ts)
         ps :: TypeParams
ps = Params { pDecl :: [TParam]
pDecl = [TParam]
as, pUse :: [Prop]
pUse = [Prop]
ts, pSubst :: Map TParam Prop
pSubst = Map TParam Prop
su }
     [Prop]
cs <- forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
ps (RO -> [Prop]
constraints RO
ro)
     forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeParams
ps,[Prop]
cs)

-- Note: we pass all value parameters as a record
newValParams :: TypeParams -> RewM (ValParams, [(Name,Type)])
newValParams :: TypeParams -> RewM (ValParams, [(Name, Prop)])
newValParams TypeParams
tps =
  do RO
ro <- forall (m :: * -> *) i. ReaderM m i => m i
ask
     let vps :: Map (MBQual Name) Prop
vps = RO -> Map (MBQual Name) Prop
vparams RO
ro
     if forall k a. Map k a -> Bool
Map.null Map (MBQual Name) Prop
vps
       then forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall decl use. Params decl use
noParams, [])
       else do [(Name, Ident, Prop)]
xts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall k a. Map k a -> [(k, a)]
Map.toList Map (MBQual Name) Prop
vps) \((Maybe ModName
q,Name
x),Prop
t) ->
                        do Prop
t1 <- forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps Prop
t
                           let l :: Ident
l = Maybe ModName -> Ident -> Ident
qualLabel Maybe ModName
q (Name -> Ident
nameIdent Name
x)
                           forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name
x, Ident
l, Prop
t1)
               let ([Name]
xs,[Ident]
ls,[Prop]
ts) = forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 [(Name, Ident, Prop)]
xts
                   fs :: [(Ident, Prop)]
fs      = forall a b. [a] -> [b] -> [(a, b)]
zip [Ident]
ls [Prop]
ts
                   sel :: Ident -> Selector
sel Ident
l   = Ident -> Maybe [Ident] -> Selector
RecordSel Ident
l (forall a. a -> Maybe a
Just [Ident]
ls)

               Prop
t <- case forall a b.
(Show a, Ord a) =>
[(a, b)] -> Either (a, b) (RecordMap a b)
recordFromFieldsErr [(Ident, Prop)]
fs of
                      Right RecordMap Ident Prop
ok -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (RecordMap Ident Prop -> Prop
TRec RecordMap Ident Prop
ok)
                      Left (Ident
x,Prop
_) ->
                        do Error -> RewM ()
recordError (BadBacktickInstance -> Error
FunctorInstanceBadBacktick
                                          (Ident -> BadBacktickInstance
BIMultipleParams Ident
x))
                           forall (f :: * -> *) a. Applicative f => a -> f a
pure (RecordMap Ident Prop -> Prop
TRec (forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields [(Ident, Prop)]
fs))

               Name
r <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift (Namespace -> Ident -> InferM Name
TC.newLocalName Namespace
NSValue (Text -> Ident
mkIdent Text
"params"))
               let e :: Expr
e = Name -> Expr
EVar Name
r
               forall (f :: * -> *) a. Applicative f => a -> f a
pure
                 ( Params
                     { pDecl :: [Name]
pDecl  = [Name
r]
                     , pUse :: [Expr]
pUse   = [Expr
e]
                     , pSubst :: Map Name Expr
pSubst = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Name
x,Expr -> Selector -> Expr
ESel Expr
e (Ident -> Selector
sel Ident
l))
                                             | (Name
x,Ident
l) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
xs [Ident]
ls ]
                     }
                 , [ (Name
r,Prop
t) ]
                 )

liftRew ::
  ((?isOurs :: Name -> Bool, ?newNewtypes :: Map Name Newtype) => a) ->
  RewM a
liftRew :: forall a.
((?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => a)
-> RewM a
liftRew (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => a
x =
  do RO
ro <- forall (m :: * -> *) i. ReaderM m i => m i
ask
     let ?isOurs      = RO -> Name -> Bool
isOurs RO
ro
         ?newNewtypes = RO -> Map Name Newtype
newNewtypes RO
ro
     forall (f :: * -> *) a. Applicative f => a -> f a
pure (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => a
x

rewTypeM :: RewType t => TypeParams -> t -> RewM t
rewTypeM :: forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
ps t
x =
  do let ?tparams = TypeParams
ps
     forall a.
((?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => a)
-> RewM a
liftRew forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure t
x

rewValM :: RewVal t => TypeParams -> Int -> ValParams -> t -> RewM t
rewValM :: forall t. RewVal t => TypeParams -> Int -> ValParams -> t -> RewM t
rewValM TypeParams
ts Int
cs ValParams
vs t
x =
  do let ?tparams = TypeParams
ts
         ?cparams = Int
cs
         ?vparams = ValParams
vs
     forall a.
((?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => a)
-> RewM a
liftRew forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure t
x

class RewType t where
  rewType ::
    ( ?isOurs      :: Name -> Bool
    , ?newNewtypes :: Map Name Newtype    -- Lazy
    , ?tparams     :: TypeParams
    ) => t -> t

instance RewType Type where
  rewType :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
Prop -> Prop
rewType Prop
ty =
    case Prop
ty of

      TCon TCon
tc [Prop]
ts
        | TC (TCAbstract (UserTC Name
x Kind
_)) <- TCon
tc
        , ?isOurs::Name -> Bool
?isOurs Name
x  -> TCon -> [Prop] -> Prop
TCon TCon
tc (forall decl use. Params decl use -> [use]
pUse ?tparams::TypeParams
?tparams forall a. [a] -> [a] -> [a]
++ forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts)
        | Bool
otherwise  -> TCon -> [Prop] -> Prop
TCon TCon
tc (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts)

      TVar TVar
x ->
        case TVar
x of
          TVBound TParam
x' ->
            case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TParam
x' (forall decl use. Params decl use -> Map decl use
pSubst ?tparams::TypeParams
?tparams) of
              Just Prop
t  -> Prop
t
              Maybe Prop
Nothing -> Prop
ty
          TVFree {} -> forall a. HasCallStack => String -> [String] -> a
panic String
"rawType" [String
"Free unification variable"]

      TUser Name
f [Prop]
ts Prop
t
        | ?isOurs::Name -> Bool
?isOurs Name
f -> Name -> [Prop] -> Prop -> Prop
TUser Name
f (forall decl use. Params decl use -> [use]
pUse ?tparams::TypeParams
?tparams forall a. [a] -> [a] -> [a]
++ forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts) (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t)
        | Bool
otherwise -> Name -> [Prop] -> Prop -> Prop
TUser Name
f (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts) (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t)

      TRec RecordMap Ident Prop
fs -> RecordMap Ident Prop -> Prop
TRec (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType RecordMap Ident Prop
fs)

      TNewtype Newtype
tdef [Prop]
ts
        | ?isOurs::Name -> Bool
?isOurs Name
nm -> Newtype -> [Prop] -> Prop
TNewtype Newtype
tdef' (forall decl use. Params decl use -> [use]
pUse ?tparams::TypeParams
?tparams forall a. [a] -> [a] -> [a]
++ forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts)
        | Bool
otherwise  -> Newtype -> [Prop] -> Prop
TNewtype Newtype
tdef (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts)
        where
        nm :: Name
nm    = Newtype -> Name
ntName Newtype
tdef
        tdef' :: Newtype
tdef' = case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
nm ?newNewtypes::Map Name Newtype
?newNewtypes of
                  Just Newtype
yes -> Newtype
yes
                  Maybe Newtype
Nothing  -> forall a. HasCallStack => String -> [String] -> a
panic String
"rewType" [ String
"Missing recursive newtype"
                                              , forall a. Show a => a -> String
show (forall a. PP a => a -> Doc
pp Name
nm) ]

instance RewType a => RewType [a] where
  rewType :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
[a] -> [a]
rewType = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType

instance RewType b => RewType (RecordMap a b) where
  rewType :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
RecordMap a b -> RecordMap a b
rewType = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType

instance RewType Schema where
  rewType :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
Schema -> Schema
rewType Schema
sch =
    Forall { sVars :: [TParam]
sVars  = Schema -> [TParam]
sVars Schema
sch
           , sProps :: [Prop]
sProps = forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType (Schema -> [Prop]
sProps Schema
sch)
           , sType :: Prop
sType  = forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType (Schema -> Prop
sType Schema
sch)
           }


class RewVal t where
  rew ::
    ( ?isOurs      :: Name -> Bool
    , ?newNewtypes :: Map Name Newtype    -- Lazy
    , ?tparams     :: TypeParams
    , ?cparams     :: Int                 -- Number of constraitns
    , ?vparams     :: ValParams
    ) => t -> t

instance RewVal a => RewVal [a] where
  rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
[a] -> [a]
rew = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew

instance RewVal b => RewVal (RecordMap a b) where
  rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
RecordMap a b -> RecordMap a b
rew = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew

{- x as cs vs  -->
   e (newAs ++ as) (newCS ++ cs) (newVS ++ vs)
-}
instance RewVal Expr where
  rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
Expr -> Expr
rew Expr
expr =
    case Expr
expr of
      EList [Expr]
es Prop
t        -> [Expr] -> Prop -> Expr
EList (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew [Expr]
es) (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t)
      ETuple [Expr]
es         -> [Expr] -> Expr
ETuple (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew [Expr]
es)
      ERec RecordMap Ident Expr
fs           -> RecordMap Ident Expr -> Expr
ERec (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew RecordMap Ident Expr
fs)
      ESel Expr
e Selector
l          -> Expr -> Selector -> Expr
ESel (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e) Selector
l
      ESet Prop
t Expr
e1 Selector
s Expr
e2    -> Prop -> Expr -> Selector -> Expr -> Expr
ESet (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e1) Selector
s (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e2)
      EIf Expr
e1 Expr
e2 Expr
e3      -> Expr -> Expr -> Expr -> Expr
EIf (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e1) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e2) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e3)
      EComp Prop
t1 Prop
t2 Expr
e [[Match]]
mss -> Prop -> Prop -> Expr -> [[Match]] -> Expr
EComp (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t1) (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t2) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew [[Match]]
mss)
      EVar Name
x            -> forall {decl}.
(?tparams::TypeParams, ?isOurs::Name -> Bool,
 ?vparams::Params decl Expr, ?newNewtypes::Map Name Newtype,
 ?cparams::Int) =>
Expr -> Expr
tryVarApp
                           case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x (forall decl use. Params decl use -> Map decl use
pSubst ?vparams::ValParams
?vparams) of
                             Just Expr
p  -> Expr
p
                             Maybe Expr
Nothing -> Expr
expr

      ETApp Expr
e Prop
t         -> forall {decl}.
(?tparams::TypeParams, ?isOurs::Name -> Bool,
 ?vparams::Params decl Expr, ?newNewtypes::Map Name Newtype,
 ?cparams::Int) =>
Expr -> Expr
tryVarApp (Expr -> Prop -> Expr
ETApp (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e) (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t))
      EProofApp Expr
e       -> forall {decl}.
(?tparams::TypeParams, ?isOurs::Name -> Bool,
 ?vparams::Params decl Expr, ?newNewtypes::Map Name Newtype,
 ?cparams::Int) =>
Expr -> Expr
tryVarApp (Expr -> Expr
EProofApp (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e))

      EApp Expr
e1 Expr
e2        -> Expr -> Expr -> Expr
EApp (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e1) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e2)
      ETAbs TParam
a Expr
e         -> TParam -> Expr -> Expr
ETAbs TParam
a (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e)
      EAbs Name
x Prop
t Expr
e        -> Name -> Prop -> Expr -> Expr
EAbs Name
x (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e)
      ELocated Range
r Expr
e      -> Range -> Expr -> Expr
ELocated Range
r (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e)
      EProofAbs Prop
p Expr
e     -> Prop -> Expr -> Expr
EProofAbs (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
p) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e)
      EWhere Expr
e [DeclGroup]
ds       -> Expr -> [DeclGroup] -> Expr
EWhere (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew [DeclGroup]
ds)
      EPropGuards [([Prop], Expr)]
gs Prop
t  -> [([Prop], Expr)] -> Prop -> Expr
EPropGuards [([Prop], Expr)]
gs' (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t)
        where gs' :: [([Prop], Expr)]
gs' = [ (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Prop]
p, forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e) | ([Prop]
p,Expr
e) <- [([Prop], Expr)]
gs ]

    where
    tryVarApp :: Expr -> Expr
tryVarApp Expr
orElse =
      case Expr -> (Expr, [Prop], Int)
splitExprInst Expr
expr of
        (EVar Name
x, [Prop]
ts, Int
cs) | ?isOurs::Name -> Bool
?isOurs Name
x ->
           let ets :: Expr
ets = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Prop -> Expr
ETApp (Name -> Expr
EVar Name
x) (forall decl use. Params decl use -> [use]
pUse ?tparams::TypeParams
?tparams forall a. [a] -> [a] -> [a]
++ forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts)
               eps :: Expr
eps = forall a. (a -> a) -> a -> [a]
iterate Expr -> Expr
EProofApp Expr
ets forall a. [a] -> Int -> a
!! (?cparams::Int
?cparams forall a. Num a => a -> a -> a
+ Int
cs)
               evs :: Expr
evs = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Expr -> Expr
EApp Expr
eps (forall decl use. Params decl use -> [use]
pUse ?vparams::Params decl Expr
?vparams)
           in Expr
evs
        (Expr, [Prop], Int)
_ -> Expr
orElse


instance RewVal DeclGroup where
  rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
DeclGroup -> DeclGroup
rew DeclGroup
dg =
    case DeclGroup
dg of
      Recursive [Decl]
ds    -> [Decl] -> DeclGroup
Recursive (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew [Decl]
ds)
      NonRecursive Decl
d  -> Decl -> DeclGroup
NonRecursive (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Decl
d)

instance RewVal Decl where
  rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
Decl -> Decl
rew Decl
d = Decl
d { dDefinition :: DeclDef
dDefinition = forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew (Decl -> DeclDef
dDefinition Decl
d)
            , dSignature :: Schema
dSignature  = forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType (Decl -> Schema
dSignature Decl
d)
            }

instance RewVal DeclDef where
  rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
DeclDef -> DeclDef
rew DeclDef
def =
    case DeclDef
def of
      DeclDef
DPrim       -> DeclDef
def
      DForeign {} -> DeclDef
def
      DExpr Expr
e     -> Expr -> DeclDef
DExpr (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e)

instance RewVal Match where
  rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
Match -> Match
rew Match
ma =
    case Match
ma of
      From Name
x Prop
t1 Prop
t2 Expr
e -> Name -> Prop -> Prop -> Expr -> Match
From Name
x (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t1) (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t2) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e)
      Let Decl
d          -> Decl -> Match
Let (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Decl
d)