{-# 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
  | Set (MBQual TParam) -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set (MBQual TParam)
as Bool -> Bool -> Bool
&& [Prop] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Prop]
ps Bool -> Bool -> Bool
&& Map (MBQual Name) Prop -> Bool
forall k a. Map k a -> Bool
Map.null Map (MBQual Name) Prop
mp = ModuleG (Located (ImpName Name))
-> InferM (ModuleG (Located (ImpName Name)))
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModuleG (Located (ImpName Name))
m
  | Bool
otherwise =
    RO
-> ReaderT RO InferM (ModuleG (Located (ImpName Name)))
-> InferM (ModuleG (Located (ImpName Name)))
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 = Set (MBQual TParam) -> [MBQual TParam]
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 = Map Name Newtype
forall k a. Map k a
Map.empty
         }

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

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

       ModuleG (Located (ImpName Name))
-> ReaderT RO InferM (ModuleG (Located (ImpName Name)))
forall a. a -> ReaderT RO InferM a
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 = (ModuleG (Located (ImpName Name)) -> Map Name (ModuleG Name))
-> BIWhat -> [(BIWhat, Name)]
forall {b} {a} {a}.
(ModuleG (Located (ImpName Name)) -> Map b a) -> a -> [(a, b)]
mkBad ModuleG (Located (ImpName Name)) -> Map Name (ModuleG Name)
forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors BIWhat
BIFunctor
       [(BIWhat, Name)] -> [(BIWhat, Name)] -> [(BIWhat, Name)]
forall a. [a] -> [a] -> [a]
++ (ModuleG (Located (ImpName Name)) -> Map Name AbstractType)
-> BIWhat -> [(BIWhat, Name)]
forall {b} {a} {a}.
(ModuleG (Located (ImpName Name)) -> Map b a) -> a -> [(a, b)]
mkBad ModuleG (Located (ImpName Name)) -> Map Name AbstractType
forall mname. ModuleG mname -> Map Name AbstractType
mPrimTypes BIWhat
BIAbstractType
       [(BIWhat, Name)] -> [(BIWhat, Name)] -> [(BIWhat, Name)]
forall a. [a] -> [a] -> [a]
++ (ModuleG (Located (ImpName Name)) -> Map Name ModParamNames)
-> BIWhat -> [(BIWhat, Name)]
forall {b} {a} {a}.
(ModuleG (Located (ImpName Name)) -> Map b a) -> a -> [(a, b)]
mkBad ModuleG (Located (ImpName Name)) -> Map Name ModParamNames
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 <- Map b a -> [b]
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 Located (ImpName Name) -> ImpName Name
forall a. Located a -> a
thing (ModuleG (Located (ImpName Name)) -> Located (ImpName Name)
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 =
      (RO -> RO) -> ReaderT RO InferM a -> ReaderT RO InferM a
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 }) (a -> ReaderT RO InferM a
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 -> ReaderT RO InferM ()
recordError Error
e = InferM () -> ReaderT RO InferM ()
forall (m :: * -> *) a. Monad m => m a -> ReaderT RO m a
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 = (a -> ReaderT RO InferM a) -> Map Name a -> RewM (Map Name a)
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) -> Map Name a -> m (Map Name b)
mapM a -> ReaderT RO InferM a
forall t. AddParams t => t -> RewM t
addParams

instance AddParams a => AddParams [a] where
  addParams :: [a] -> RewM [a]
addParams = (a -> ReaderT RO InferM a) -> [a] -> RewM [a]
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 a -> ReaderT RO InferM a
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   <- TypeParams -> [Prop] -> RewM [Prop]
forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (Newtype -> [Prop]
ntConstraints Newtype
nt)
       RecordMap Ident Prop
rFields  <- TypeParams -> RecordMap Ident Prop -> RewM (RecordMap Ident Prop)
forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (Newtype -> RecordMap Ident Prop
ntFields Newtype
nt)
       Newtype -> RewM Newtype
forall a. a -> ReaderT RO InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Newtype
nt
         { ntParams :: [TParam]
ntParams       = TypeParams -> [TParam]
forall decl use. Params decl use -> [decl]
pDecl TypeParams
tps [TParam] -> [TParam] -> [TParam]
forall a. [a] -> [a] -> [a]
++ Newtype -> [TParam]
ntParams Newtype
nt
         , ntConstraints :: [Prop]
ntConstraints  = [Prop]
cs [Prop] -> [Prop] -> [Prop]
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   <- TypeParams -> [Prop] -> RewM [Prop]
forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (TySyn -> [Prop]
tsConstraints TySyn
ts)
       Prop
rDef     <- TypeParams -> Prop -> RewM Prop
forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (TySyn -> Prop
tsDef TySyn
ts)
       TySyn -> RewM TySyn
forall a. a -> ReaderT RO InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TySyn
ts
         { tsParams :: [TParam]
tsParams      = TypeParams -> [TParam]
forall decl use. Params decl use -> [decl]
pDecl TypeParams
tps [TParam] -> [TParam] -> [TParam]
forall a. [a] -> [a] -> [a]
++ TySyn -> [TParam]
tsParams TySyn
ts
         , tsConstraints :: [Prop]
tsConstraints = [Prop]
cs [Prop] -> [Prop] -> [Prop]
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 ([Decl] -> DeclGroup) -> ReaderT RO InferM [Decl] -> RewM DeclGroup
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Decl] -> ReaderT RO InferM [Decl]
forall t. AddParams t => t -> RewM t
addParams [Decl]
ds
      NonRecursive Decl
d -> Decl -> DeclGroup
NonRecursive (Decl -> DeclGroup) -> ReaderT RO InferM Decl -> RewM DeclGroup
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Decl -> ReaderT RO InferM Decl
forall t. AddParams t => t -> RewM t
addParams Decl
d

instance AddParams Decl where
  addParams :: Decl -> ReaderT RO InferM Decl
addParams Decl
d =
    case Decl -> DeclDef
dDefinition Decl
d of
      DeclDef
DPrim       -> BIWhat -> ReaderT RO InferM Decl
bad BIWhat
BIPrimitive
      DForeign {} -> BIWhat -> ReaderT RO InferM 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 <- TypeParams -> Prop -> RewM Prop
forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (Schema -> Prop
sType Schema
s)
           [Prop]
ps1 <- TypeParams -> [Prop] -> RewM [Prop]
forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (Schema -> [Prop]
sProps Schema
s)
           let ty2 :: Prop
ty2 = (Prop -> Prop -> Prop) -> Prop -> [Prop] -> Prop
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Prop -> Prop
tFun Prop
ty1 (((Name, Prop) -> Prop) -> [(Name, Prop)] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Prop) -> Prop
forall a b. (a, b) -> b
snd [(Name, Prop)]
bs)

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

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

           Decl -> ReaderT RO InferM Decl
forall a. a -> ReaderT RO InferM a
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 -> ReaderT RO InferM Decl
bad BIWhat
w =
      do Error -> ReaderT RO InferM ()
recordError (BadBacktickInstance -> Error
FunctorInstanceBadBacktick ([(BIWhat, Name)] -> BadBacktickInstance
BINested [(BIWhat
w,Decl -> Name
dName Decl
d)]))
         Decl -> ReaderT RO InferM Decl
forall a. a -> ReaderT RO InferM a
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  = Map decl use
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 [Text] -> [Text] -> [Text]
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 <- ReaderT RO InferM RO
forall (m :: * -> *) i. ReaderM m i => m i
ask
     let newFlaf :: Maybe ModName -> Name -> TPFlavor
newFlaf Maybe ModName
q = Name -> TPFlavor
flav (Name -> TPFlavor) -> (Name -> Name) -> Name -> TPFlavor
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 <- InferM [TParam] -> ReaderT RO InferM [TParam]
forall (m :: * -> *) a. Monad m => m a -> ReaderT RO m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift ([MBQual TParam]
-> (MBQual TParam -> InferM TParam) -> InferM [TParam]
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]
_ <- [Ident] -> [[Ident]]
forall a. Eq a => [a] -> [[a]]
group ([Ident] -> [Ident]
forall a. Ord a => [a] -> [a]
sort ((Name -> Ident) -> [Name] -> [Ident]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Ident
nameIdent ((TParam -> Maybe Name) -> [TParam] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TParam -> Maybe Name
tpName [TParam]
as)))
               ]
     [Ident] -> (Ident -> ReaderT RO InferM ()) -> ReaderT RO InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Ident]
bad \Ident
i ->
       Error -> ReaderT RO InferM ()
recordError (BadBacktickInstance -> Error
FunctorInstanceBadBacktick (Ident -> BadBacktickInstance
BIMultipleParams Ident
i))

     let ts :: [Prop]
ts = (TParam -> Prop) -> [TParam] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map (TVar -> Prop
TVar (TVar -> Prop) -> (TParam -> TVar) -> TParam -> Prop
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> TVar
TVBound) [TParam]
as
         su :: Map TParam Prop
su = [(TParam, Prop)] -> Map TParam Prop
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([TParam] -> [Prop] -> [(TParam, Prop)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((MBQual TParam -> TParam) -> [MBQual TParam] -> [TParam]
forall a b. (a -> b) -> [a] -> [b]
map MBQual TParam -> TParam
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 <- TypeParams -> [Prop] -> RewM [Prop]
forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
ps (RO -> [Prop]
constraints RO
ro)
     (TypeParams, [Prop]) -> RewM (TypeParams, [Prop])
forall a. a -> ReaderT RO InferM a
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 <- ReaderT RO InferM 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 Map (MBQual Name) Prop -> Bool
forall k a. Map k a -> Bool
Map.null Map (MBQual Name) Prop
vps
       then (ValParams, [(Name, Prop)]) -> RewM (ValParams, [(Name, Prop)])
forall a. a -> ReaderT RO InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ValParams
forall decl use. Params decl use
noParams, [])
       else do [(Name, Ident, Prop)]
xts <- [(MBQual Name, Prop)]
-> ((MBQual Name, Prop) -> ReaderT RO InferM (Name, Ident, Prop))
-> ReaderT RO InferM [(Name, Ident, Prop)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Map (MBQual Name) Prop -> [(MBQual Name, Prop)]
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 <- TypeParams -> Prop -> RewM Prop
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)
                           (Name, Ident, Prop) -> ReaderT RO InferM (Name, Ident, Prop)
forall a. a -> ReaderT RO InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name
x, Ident
l, Prop
t1)
               let ([Name]
xs,[Ident]
ls,[Prop]
ts) = [(Name, Ident, Prop)] -> ([Name], [Ident], [Prop])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 [(Name, Ident, Prop)]
xts
                   fs :: [(Ident, Prop)]
fs      = [Ident] -> [Prop] -> [(Ident, Prop)]
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 ([Ident] -> Maybe [Ident]
forall a. a -> Maybe a
Just [Ident]
ls)

               Prop
t <- case [(Ident, Prop)] -> Either (Ident, Prop) (RecordMap Ident Prop)
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 -> Prop -> RewM Prop
forall a. a -> ReaderT RO InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RecordMap Ident Prop -> Prop
TRec RecordMap Ident Prop
ok)
                      Left (Ident
x,Prop
_) ->
                        do Error -> ReaderT RO InferM ()
recordError (BadBacktickInstance -> Error
FunctorInstanceBadBacktick
                                          (Ident -> BadBacktickInstance
BIMultipleParams Ident
x))
                           Prop -> RewM Prop
forall a. a -> ReaderT RO InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RecordMap Ident Prop -> Prop
TRec ([(Ident, Prop)] -> RecordMap Ident Prop
forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields [(Ident, Prop)]
fs))

               Name
r <- InferM Name -> ReaderT RO InferM Name
forall (m :: * -> *) a. Monad m => m a -> ReaderT RO m a
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
               (ValParams, [(Name, Prop)]) -> RewM (ValParams, [(Name, Prop)])
forall a. a -> ReaderT RO InferM a
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 = [(Name, Expr)] -> Map Name Expr
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) <- [Name] -> [Ident] -> [(Name, Ident)]
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 <- ReaderT RO InferM 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
     a -> RewM a
forall a. a -> ReaderT RO InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
(?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 = ?tparams::TypeParams
TypeParams
ps
     ((?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => t -> t)
-> RewM (t -> t)
forall a.
((?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => a)
-> RewM a
liftRew t -> t
(?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => t -> t
forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType RewM (t -> t) -> RewM t -> RewM t
forall a b.
ReaderT RO InferM (a -> b)
-> ReaderT RO InferM a -> ReaderT RO InferM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> RewM t
forall a. a -> ReaderT RO InferM a
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 = ?tparams::TypeParams
TypeParams
ts
         ?cparams = ?cparams::Int
Int
cs
         ?vparams = ?vparams::ValParams
ValParams
vs
     ((?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => t -> t)
-> RewM (t -> t)
forall a.
((?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => a)
-> RewM a
liftRew t -> t
(?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => t -> t
forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew RewM (t -> t) -> RewM t -> RewM t
forall a b.
ReaderT RO InferM (a -> b)
-> ReaderT RO InferM a -> ReaderT RO InferM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> RewM t
forall a. a -> ReaderT RO InferM a
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
Name -> Bool
?isOurs Name
x  -> TCon -> [Prop] -> Prop
TCon TCon
tc (TypeParams -> [Prop]
forall decl use. Params decl use -> [use]
pUse ?tparams::TypeParams
TypeParams
?tparams [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop] -> [Prop]
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 ([Prop] -> [Prop]
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 TParam -> Map TParam Prop -> Maybe Prop
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TParam
x' (TypeParams -> Map TParam Prop
forall decl use. Params decl use -> Map decl use
pSubst ?tparams::TypeParams
TypeParams
?tparams) of
              Just Prop
t  -> Prop
t
              Maybe Prop
Nothing -> Prop
ty
          TVFree {} -> String -> [String] -> Prop
forall a. HasCallStack => String -> [String] -> a
panic String
"rawType" [String
"Free unification variable"]

      TUser Name
f [Prop]
ts Prop
t
        | ?isOurs::Name -> Bool
Name -> Bool
?isOurs Name
f -> Name -> [Prop] -> Prop -> Prop
TUser Name
f (TypeParams -> [Prop]
forall decl use. Params decl use -> [use]
pUse ?tparams::TypeParams
TypeParams
?tparams [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop] -> [Prop]
forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts) (Prop -> Prop
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 ([Prop] -> [Prop]
forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts) (Prop -> Prop
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 (RecordMap Ident Prop -> RecordMap Ident Prop
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
Name -> Bool
?isOurs Name
nm -> Newtype -> [Prop] -> Prop
TNewtype Newtype
tdef' (TypeParams -> [Prop]
forall decl use. Params decl use -> [use]
pUse ?tparams::TypeParams
TypeParams
?tparams [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop] -> [Prop]
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 ([Prop] -> [Prop]
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 Name -> Map Name Newtype -> Maybe Newtype
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
nm ?newNewtypes::Map Name Newtype
Map Name Newtype
?newNewtypes of
                  Just Newtype
yes -> Newtype
yes
                  Maybe Newtype
Nothing  -> String -> [String] -> Newtype
forall a. HasCallStack => String -> [String] -> a
panic String
"rewType" [ String
"Missing recursive newtype"
                                              , Doc -> String
forall a. Show a => a -> String
show (Name -> Doc
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 = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a
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 = (b -> b) -> RecordMap a b -> RecordMap a b
forall a b. (a -> b) -> RecordMap a a -> RecordMap a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> b
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 = [Prop] -> [Prop]
forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType (Schema -> [Prop]
sProps Schema
sch)
           , sType :: Prop
sType  = Prop -> Prop
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 = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a
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 = (b -> b) -> RecordMap a b -> RecordMap a b
forall a b. (a -> b) -> RecordMap a a -> RecordMap a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> b
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 ([Expr] -> [Expr]
forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew [Expr]
es) (Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t)
      ETuple [Expr]
es         -> [Expr] -> Expr
ETuple ([Expr] -> [Expr]
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 (RecordMap Ident Expr -> RecordMap Ident Expr
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 (Expr -> Expr
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 (Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t) (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e1) Selector
s (Expr -> Expr
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 (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e1) (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e2) (Expr -> Expr
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 (Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t1) (Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t2) (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e) ([[Match]] -> [[Match]]
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            -> Expr -> Expr
forall {decl}.
(?tparams::TypeParams, ?isOurs::Name -> Bool,
 ?vparams::Params decl Expr, ?newNewtypes::Map Name Newtype,
 ?cparams::Int) =>
Expr -> Expr
tryVarApp
                           case Name -> Map Name Expr -> Maybe Expr
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x (ValParams -> Map Name Expr
forall decl use. Params decl use -> Map decl use
pSubst ?vparams::ValParams
ValParams
?vparams) of
                             Just Expr
p  -> Expr
p
                             Maybe Expr
Nothing -> Expr
expr

      ETApp Expr
e Prop
t         -> Expr -> Expr
forall {decl}.
(?tparams::TypeParams, ?isOurs::Name -> Bool,
 ?vparams::Params decl Expr, ?newNewtypes::Map Name Newtype,
 ?cparams::Int) =>
Expr -> Expr
tryVarApp (Expr -> Prop -> Expr
ETApp (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e) (Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t))
      EProofApp Expr
e       -> Expr -> Expr
forall {decl}.
(?tparams::TypeParams, ?isOurs::Name -> Bool,
 ?vparams::Params decl Expr, ?newNewtypes::Map Name Newtype,
 ?cparams::Int) =>
Expr -> Expr
tryVarApp (Expr -> Expr
EProofApp (Expr -> Expr
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 (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e1) (Expr -> Expr
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 (Expr -> Expr
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 (Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t) (Expr -> Expr
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 (Expr -> Expr
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 (Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
p) (Expr -> Expr
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 (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e) ([DeclGroup] -> [DeclGroup]
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' (Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t)
        where gs' :: [([Prop], Expr)]
gs' = [ (Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType (Prop -> Prop) -> [Prop] -> [Prop]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Prop]
p, Expr -> Expr
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
Name -> Bool
?isOurs Name
x ->
           let ets :: Expr
ets = (Expr -> Prop -> Expr) -> Expr -> [Prop] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Prop -> Expr
ETApp (Name -> Expr
EVar Name
x) (TypeParams -> [Prop]
forall decl use. Params decl use -> [use]
pUse ?tparams::TypeParams
TypeParams
?tparams [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop] -> [Prop]
forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts)
               eps :: Expr
eps = (Expr -> Expr) -> Expr -> [Expr]
forall a. (a -> a) -> a -> [a]
iterate Expr -> Expr
EProofApp Expr
ets [Expr] -> Int -> Expr
forall a. HasCallStack => [a] -> Int -> a
!! (?cparams::Int
Int
?cparams Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
cs)
               evs :: Expr
evs = (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Expr -> Expr
EApp Expr
eps (Params decl Expr -> [Expr]
forall decl use. Params decl use -> [use]
pUse ?vparams::Params decl Expr
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 ([Decl] -> [Decl]
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 (Decl -> Decl
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 = DeclDef -> DeclDef
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  = Schema -> Schema
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 (Expr -> Expr
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 (Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t1) (Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams) =>
t -> t
rewType Prop
t2) (Expr -> Expr
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 (Decl -> Decl
forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Decl
d)