{-# 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(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.AST(impNameModPath)
import Cryptol.Parser.Position
import Cryptol.ModuleSystem.Name(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
         , newNominalTypes :: Map Name NominalType
newNominalTypes = Map Name NominalType
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 NominalType
-> (ModuleG (Located (ImpName Name)) -> Map Name TySyn)
-> ReaderT RO InferM (Map Name TySyn)
forall {a}.
AddParams a =>
Map Name NominalType
-> (ModuleG (Located (ImpName Name)) -> a) -> ReaderT RO InferM a
doAddParams Map Name NominalType
nt ModuleG (Located (ImpName Name)) -> Map Name TySyn
forall mname. ModuleG mname -> Map Name TySyn
mTySyns
         Map Name NominalType
nt <- Map Name NominalType
-> (ModuleG (Located (ImpName Name)) -> Map Name NominalType)
-> ReaderT RO InferM (Map Name NominalType)
forall {a}.
AddParams a =>
Map Name NominalType
-> (ModuleG (Located (ImpName Name)) -> a) -> ReaderT RO InferM a
doAddParams Map Name NominalType
nt ModuleG (Located (ImpName Name)) -> Map Name NominalType
forall mname. ModuleG mname -> Map Name NominalType
mNominalTypes
         [DeclGroup]
ds <- Map Name NominalType
-> (ModuleG (Located (ImpName Name)) -> [DeclGroup])
-> ReaderT RO InferM [DeclGroup]
forall {a}.
AddParams a =>
Map Name NominalType
-> (ModuleG (Located (ImpName Name)) -> a) -> ReaderT RO InferM a
doAddParams Map Name NominalType
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   = ts
         , mNominalTypes = nt
         , mDecls    = 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 NominalType)
-> BIWhat -> [(BIWhat, Name)]
forall {b} {a} {a}.
(ModuleG (Located (ImpName Name)) -> Map b a) -> a -> [(a, b)]
mkBad ModuleG (Located (ImpName Name)) -> Map Name NominalType
forall mname. ModuleG mname -> Map Name NominalType
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

    mPrimTypes :: ModuleG mname -> Map Name NominalType
mPrimTypes = (NominalType -> Bool)
-> Map Name NominalType -> Map Name NominalType
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter NominalType -> Bool
nominalTypeIsAbstract (Map Name NominalType -> Map Name NominalType)
-> (ModuleG mname -> Map Name NominalType)
-> ModuleG mname
-> Map Name NominalType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleG mname -> Map Name NominalType
forall mname. ModuleG mname -> Map Name NominalType
mNominalTypes

    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 = ImpName Name -> ModPath
impNameModPath (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))

    doAddParams :: Map Name NominalType
-> (ModuleG (Located (ImpName Name)) -> a) -> ReaderT RO InferM a
doAddParams Map Name NominalType
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 { newNominalTypes = 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 NominalType
newNominalTypes :: Map Name NominalType
  }


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 NominalType where
  addParams :: NominalType -> RewM NominalType
addParams NominalType
nt =
    do (TypeParams
tps,[Prop]
cs) <- (Name -> TPFlavor) -> RewM (TypeParams, [Prop])
newTypeParams Name -> TPFlavor
TPNominalParam
       [Prop]
rProps   <- TypeParams -> [Prop] -> RewM [Prop]
forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (NominalType -> [Prop]
ntConstraints NominalType
nt)
       NominalTypeDef
def <- case NominalType -> NominalTypeDef
ntDef NominalType
nt of
                Struct StructCon
con ->
                   StructCon -> NominalTypeDef
Struct (StructCon -> NominalTypeDef)
-> ReaderT RO InferM StructCon -> ReaderT RO InferM NominalTypeDef
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                   do RecordMap Ident Prop
rFields  <- TypeParams -> RecordMap Ident Prop -> RewM (RecordMap Ident Prop)
forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (StructCon -> RecordMap Ident Prop
ntFields StructCon
con)
                      StructCon -> ReaderT RO InferM StructCon
forall a. a -> ReaderT RO InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure StructCon
con { ntFields = rFields }
                Enum [EnumCon]
cons ->
                  [EnumCon] -> NominalTypeDef
Enum ([EnumCon] -> NominalTypeDef)
-> ReaderT RO InferM [EnumCon] -> ReaderT RO InferM NominalTypeDef
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                  [EnumCon]
-> (EnumCon -> ReaderT RO InferM EnumCon)
-> ReaderT RO InferM [EnumCon]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [EnumCon]
cons \EnumCon
c ->
                    do [Prop]
rFileds <- TypeParams -> [Prop] -> RewM [Prop]
forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (EnumCon -> [Prop]
ecFields EnumCon
c)
                       EnumCon -> ReaderT RO InferM EnumCon
forall a. a -> ReaderT RO InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure EnumCon
c { ecFields = rFileds }
                NominalTypeDef
Abstract -> NominalTypeDef -> ReaderT RO InferM NominalTypeDef
forall a. a -> ReaderT RO InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure NominalTypeDef
Abstract
       NominalType -> RewM NominalType
forall a. a -> ReaderT RO InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure NominalType
nt
         { ntParams      = pDecl tps ++ ntParams nt
         , ntConstraints = cs ++ rProps
         , ntDef         = def
         }


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      = pDecl tps ++ tsParams ts
         , tsConstraints = cs ++ rProps
         , tsDef         = 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 = DExpr e6
                  , dSignature  = 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, ?newNominalTypes :: Map Name NominalType) => a) ->
  RewM a
liftRew :: forall a.
((?isOurs::Name -> Bool, ?newNominalTypes::Map Name NominalType) =>
 a)
-> RewM a
liftRew (?isOurs::Name -> Bool, ?newNominalTypes::Map Name NominalType) =>
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
         ?newNominalTypes = RO -> Map Name NominalType
newNominalTypes 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, ?newNominalTypes::Map Name NominalType) =>
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, ?newNominalTypes::Map Name NominalType) =>
 t -> t)
-> RewM (t -> t)
forall a.
((?isOurs::Name -> Bool, ?newNominalTypes::Map Name NominalType) =>
 a)
-> RewM a
liftRew t -> t
(?isOurs::Name -> Bool, ?newNominalTypes::Map Name NominalType) =>
t -> t
forall t.
(RewType t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?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, ?newNominalTypes::Map Name NominalType) =>
 t -> t)
-> RewM (t -> t)
forall a.
((?isOurs::Name -> Bool, ?newNominalTypes::Map Name NominalType) =>
 a)
-> RewM a
liftRew t -> t
(?isOurs::Name -> Bool, ?newNominalTypes::Map Name NominalType) =>
t -> t
forall t.
(RewVal t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?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
    , ?newNominalTypes :: Map Name NominalType -- Lazy
    , ?tparams     :: TypeParams
    ) => t -> t

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

      TCon TCon
tc [Prop]
ts -> TCon -> [Prop] -> Prop
TCon TCon
tc ([Prop] -> [Prop]
forall t.
(RewType t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts) (Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts) (Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams) =>
t -> t
rewType RecordMap Ident Prop
fs)

      TNominal NominalType
tdef [Prop]
ts
        | ?isOurs::Name -> Bool
Name -> Bool
?isOurs Name
nm -> NominalType -> [Prop] -> Prop
TNominal NominalType
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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts)
        | Bool
otherwise  -> NominalType -> [Prop] -> Prop
TNominal NominalType
tdef ([Prop] -> [Prop]
forall t.
(RewType t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts)
        where
        nm :: Name
nm    = NominalType -> Name
ntName NominalType
tdef
        tdef' :: NominalType
tdef' = case Name -> Map Name NominalType -> Maybe NominalType
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
nm ?newNominalTypes::Map Name NominalType
Map Name NominalType
?newNominalTypes of
                  Just NominalType
yes -> NominalType
yes
                  Maybe NominalType
Nothing  -> String -> [String] -> NominalType
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, ?newNominalTypes::Map Name NominalType,
 ?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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams) =>
t -> t
rewType

instance RewType b => RewType (RecordMap a b) where
  rewType :: (?isOurs::Name -> Bool, ?newNominalTypes::Map Name NominalType,
 ?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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams) =>
t -> t
rewType

instance RewType Schema where
  rewType :: (?isOurs::Name -> Bool, ?newNominalTypes::Map Name NominalType,
 ?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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams) =>
t -> t
rewType (Schema -> [Prop]
sProps Schema
sch)
           , sType :: Prop
sType  = Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams) =>
t -> t
rewType (Schema -> Prop
sType Schema
sch)
           }


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

instance RewVal a => RewVal [a] where
  rew :: (?isOurs::Name -> Bool, ?newNominalTypes::Map Name NominalType,
 ?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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams,
 ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew

instance RewVal b => RewVal (RecordMap a b) where
  rew :: (?isOurs::Name -> Bool, ?newNominalTypes::Map Name NominalType,
 ?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,
 ?newNominalTypes::Map Name NominalType, ?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, ?newNominalTypes::Map Name NominalType,
 ?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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams,
 ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew [Expr]
es) (Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams) =>
t -> t
rewType Prop
t)
      ETuple [Expr]
es         -> [Expr] -> Expr
ETuple ([Expr] -> [Expr]
forall t.
(RewVal t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?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,
 ?newNominalTypes::Map Name NominalType, ?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,
 ?newNominalTypes::Map Name NominalType, ?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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams) =>
t -> t
rewType Prop
t) (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams,
 ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e1) Selector
s (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams,
 ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e1) (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams,
 ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e2) (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams,
 ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e3)
      ECase Expr
e Map Ident CaseAlt
as Maybe CaseAlt
d      -> Expr -> Map Ident CaseAlt -> Maybe CaseAlt -> Expr
ECase (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams,
 ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e) (CaseAlt -> CaseAlt
forall t.
(RewVal t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams,
 ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew (CaseAlt -> CaseAlt) -> Map Ident CaseAlt -> Map Ident CaseAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Ident CaseAlt
as) (CaseAlt -> CaseAlt
forall t.
(RewVal t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams,
 ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew (CaseAlt -> CaseAlt) -> Maybe CaseAlt -> Maybe CaseAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe CaseAlt
d)
      EComp Prop
t1 Prop
t2 Expr
e [[Match]]
mss -> Prop -> Prop -> Expr -> [[Match]] -> Expr
EComp (Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams) =>
t -> t
rewType Prop
t1) (Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams) =>
t -> t
rewType Prop
t2) (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams,
 ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e) ([[Match]] -> [[Match]]
forall t.
(RewVal t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?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, ?newNominalTypes::Map Name NominalType,
 ?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, ?newNominalTypes::Map Name NominalType,
 ?cparams::Int) =>
Expr -> Expr
tryVarApp (Expr -> Prop -> Expr
ETApp (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams,
 ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e) (Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams) =>
t -> t
rewType Prop
t))
      EProofApp Expr
e       -> Expr -> Expr
forall {decl}.
(?tparams::TypeParams, ?isOurs::Name -> Bool,
 ?vparams::Params decl Expr, ?newNominalTypes::Map Name NominalType,
 ?cparams::Int) =>
Expr -> Expr
tryVarApp (Expr -> Expr
EProofApp (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams,
 ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e1) (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?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,
 ?newNominalTypes::Map Name NominalType, ?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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams) =>
t -> t
rewType Prop
t) (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?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,
 ?newNominalTypes::Map Name NominalType, ?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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams) =>
t -> t
rewType Prop
p) (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams,
 ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e) ([DeclGroup] -> [DeclGroup]
forall t.
(RewVal t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams) =>
t -> t
rewType Prop
t)
        where gs' :: [([Prop], Expr)]
gs' = [ (Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?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,
 ?newNominalTypes::Map Name NominalType, ?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,
 ?newNominalTypes::Map Name NominalType, ?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 CaseAlt where
  rew :: (?isOurs::Name -> Bool, ?newNominalTypes::Map Name NominalType,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
CaseAlt -> CaseAlt
rew (CaseAlt [(Name, Prop)]
xs Expr
e) = [(Name, Prop)] -> Expr -> CaseAlt
CaseAlt [(Name, Prop)]
xs (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams,
 ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e)


instance RewVal DeclGroup where
  rew :: (?isOurs::Name -> Bool, ?newNominalTypes::Map Name NominalType,
 ?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,
 ?newNominalTypes::Map Name NominalType, ?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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams,
 ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Decl
d)

instance RewVal Decl where
  rew :: (?isOurs::Name -> Bool, ?newNominalTypes::Map Name NominalType,
 ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
Decl -> Decl
rew Decl
d = Decl
d { dDefinition = rew (dDefinition d)
            , dSignature  = rewType (dSignature d)
            }

instance RewVal DeclDef where
  rew :: (?isOurs::Name -> Bool, ?newNominalTypes::Map Name NominalType,
 ?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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams,
 ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e)

instance RewVal Match where
  rew :: (?isOurs::Name -> Bool, ?newNominalTypes::Map Name NominalType,
 ?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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams) =>
t -> t
rewType Prop
t1) (Prop -> Prop
forall t.
(RewType t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams) =>
t -> t
rewType Prop
t2) (Expr -> Expr
forall t.
(RewVal t, ?isOurs::Name -> Bool,
 ?newNominalTypes::Map Name NominalType, ?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,
 ?newNominalTypes::Map Name NominalType, ?tparams::TypeParams,
 ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Decl
d)