{-# 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)
doBacktickInstance ::
Set (MBQual TParam) ->
[Prop] ->
Map (MBQual Name) Type ->
ModuleG (Located (ImpName Name)) ->
TC.InferM (ModuleG (Located (ImpName Name)))
doBacktickInstance :: Set (MBQual TParam)
-> [Prop]
-> Map (MBQual Name) Prop
-> ModuleG (Located (ImpName Name))
-> InferM (ModuleG (Located (ImpName Name)))
doBacktickInstance Set (MBQual TParam)
as [Prop]
ps Map (MBQual Name) Prop
mp ModuleG (Located (ImpName Name))
m
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set (MBQual TParam)
as Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Prop]
ps Bool -> Bool -> Bool
&& forall k a. Map k a -> Bool
Map.null Map (MBQual Name) Prop
mp = forall (f :: * -> *) a. Applicative f => a -> f a
pure ModuleG (Located (ImpName Name))
m
| Bool
otherwise =
forall i (m :: * -> *) a. i -> ReaderT i m a -> m a
runReaderT
RO { isOurs :: Name -> Bool
isOurs = \Name
x -> case Name -> Maybe ModPath
nameModPathMaybe Name
x of
Maybe ModPath
Nothing -> Bool
False
Just ModPath
y -> ModPath
ourPath ModPath -> ModPath -> Bool
`modPathIsOrContains` ModPath
y
, tparams :: [MBQual TParam]
tparams = forall a. Set a -> [a]
Set.toList Set (MBQual TParam)
as
, constraints :: [Prop]
constraints = [Prop]
ps
, vparams :: Map (MBQual Name) Prop
vparams = Map (MBQual Name) Prop
mp
, newNewtypes :: Map Name Newtype
newNewtypes = forall k a. Map k a
Map.empty
}
do forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(BIWhat, Name)]
bad)
(Error -> RewM ()
recordError (BadBacktickInstance -> Error
FunctorInstanceBadBacktick ([(BIWhat, Name)] -> BadBacktickInstance
BINested [(BIWhat, Name)]
bad)))
rec
Map Name TySyn
ts <- forall {a}.
AddParams a =>
Map Name Newtype
-> (ModuleG (Located (ImpName Name)) -> a) -> ReaderT RO InferM a
doAddParams Map Name Newtype
nt forall mname. ModuleG mname -> Map Name TySyn
mTySyns
Map Name Newtype
nt <- forall {a}.
AddParams a =>
Map Name Newtype
-> (ModuleG (Located (ImpName Name)) -> a) -> ReaderT RO InferM a
doAddParams Map Name Newtype
nt forall mname. ModuleG mname -> Map Name Newtype
mNewtypes
[DeclGroup]
ds <- forall {a}.
AddParams a =>
Map Name Newtype
-> (ModuleG (Located (ImpName Name)) -> a) -> ReaderT RO InferM a
doAddParams Map Name Newtype
nt forall mname. ModuleG mname -> [DeclGroup]
mDecls
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModuleG (Located (ImpName Name))
m
{ mTySyns :: Map Name TySyn
mTySyns = Map Name TySyn
ts
, mNewtypes :: Map Name Newtype
mNewtypes = Map Name Newtype
nt
, mDecls :: [DeclGroup]
mDecls = [DeclGroup]
ds
}
where
bad :: [(BIWhat, Name)]
bad = forall {b} {a} {a}.
(ModuleG (Located (ImpName Name)) -> Map b a) -> a -> [(a, b)]
mkBad forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors BIWhat
BIFunctor
forall a. [a] -> [a] -> [a]
++ forall {b} {a} {a}.
(ModuleG (Located (ImpName Name)) -> Map b a) -> a -> [(a, b)]
mkBad forall mname. ModuleG mname -> Map Name AbstractType
mPrimTypes BIWhat
BIAbstractType
forall a. [a] -> [a] -> [a]
++ forall {b} {a} {a}.
(ModuleG (Located (ImpName Name)) -> Map b a) -> a -> [(a, b)]
mkBad forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures BIWhat
BIInterface
mkBad :: (ModuleG (Located (ImpName Name)) -> Map b a) -> a -> [(a, b)]
mkBad ModuleG (Located (ImpName Name)) -> Map b a
sel a
a = [ (a
a,b
k) | b
k <- forall k a. Map k a -> [k]
Map.keys (ModuleG (Located (ImpName Name)) -> Map b a
sel ModuleG (Located (ImpName Name))
m) ]
ourPath :: ModPath
ourPath = case forall a. Located a -> a
thing (forall mname. ModuleG mname -> mname
mName ModuleG (Located (ImpName Name))
m) of
ImpTop ModName
mo -> ModName -> ModPath
TopModule ModName
mo
ImpNested Name
mo -> ModPath -> Ident -> ModPath
Nested (Name -> ModPath
nameModPath Name
mo) (Name -> Ident
nameIdent Name
mo)
doAddParams :: Map Name Newtype
-> (ModuleG (Located (ImpName Name)) -> a) -> ReaderT RO InferM a
doAddParams Map Name Newtype
nt ModuleG (Located (ImpName Name)) -> a
sel =
forall (m :: * -> *) r a. RunReaderM m r => (r -> r) -> m a -> m a
mapReader (\RO
ro -> RO
ro { newNewtypes :: Map Name Newtype
newNewtypes = Map Name Newtype
nt }) (forall t. AddParams t => t -> RewM t
addParams (ModuleG (Located (ImpName Name)) -> a
sel ModuleG (Located (ImpName Name))
m))
type RewM = ReaderT RO TC.InferM
recordError :: Error -> RewM ()
recordError :: Error -> RewM ()
recordError Error
e = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift (Error -> InferM ()
TC.recordError Error
e)
data RO = RO
{ RO -> Name -> Bool
isOurs :: Name -> Bool
, RO -> [MBQual TParam]
tparams :: [MBQual TParam]
, RO -> [Prop]
constraints :: [Prop]
, RO -> Map (MBQual Name) Prop
vparams :: Map (MBQual Name) Type
, RO -> Map Name Newtype
newNewtypes :: Map Name Newtype
}
class AddParams t where
addParams :: t -> RewM t
instance AddParams a => AddParams (Map Name a) where
addParams :: Map Name a -> RewM (Map Name a)
addParams = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t. AddParams t => t -> RewM t
addParams
instance AddParams a => AddParams [a] where
addParams :: [a] -> RewM [a]
addParams = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t. AddParams t => t -> RewM t
addParams
instance AddParams Newtype where
addParams :: Newtype -> RewM Newtype
addParams Newtype
nt =
do (TypeParams
tps,[Prop]
cs) <- (Name -> TPFlavor) -> RewM (TypeParams, [Prop])
newTypeParams Name -> TPFlavor
TPNewtypeParam
[Prop]
rProps <- forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (Newtype -> [Prop]
ntConstraints Newtype
nt)
RecordMap Ident Prop
rFields <- forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (Newtype -> RecordMap Ident Prop
ntFields Newtype
nt)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Newtype
nt
{ ntParams :: [TParam]
ntParams = forall decl use. Params decl use -> [decl]
pDecl TypeParams
tps forall a. [a] -> [a] -> [a]
++ Newtype -> [TParam]
ntParams Newtype
nt
, ntConstraints :: [Prop]
ntConstraints = [Prop]
cs forall a. [a] -> [a] -> [a]
++ [Prop]
rProps
, ntFields :: RecordMap Ident Prop
ntFields = RecordMap Ident Prop
rFields
}
instance AddParams TySyn where
addParams :: TySyn -> RewM TySyn
addParams TySyn
ts =
do (TypeParams
tps,[Prop]
cs) <- (Name -> TPFlavor) -> RewM (TypeParams, [Prop])
newTypeParams Name -> TPFlavor
TPTySynParam
[Prop]
rProps <- forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (TySyn -> [Prop]
tsConstraints TySyn
ts)
Prop
rDef <- forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (TySyn -> Prop
tsDef TySyn
ts)
forall (f :: * -> *) a. Applicative f => a -> f a
pure TySyn
ts
{ tsParams :: [TParam]
tsParams = forall decl use. Params decl use -> [decl]
pDecl TypeParams
tps forall a. [a] -> [a] -> [a]
++ TySyn -> [TParam]
tsParams TySyn
ts
, tsConstraints :: [Prop]
tsConstraints = [Prop]
cs forall a. [a] -> [a] -> [a]
++ [Prop]
rProps
, tsDef :: Prop
tsDef = Prop
rDef
}
instance AddParams DeclGroup where
addParams :: DeclGroup -> RewM DeclGroup
addParams DeclGroup
dg =
case DeclGroup
dg of
Recursive [Decl]
ds -> [Decl] -> DeclGroup
Recursive forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. AddParams t => t -> RewM t
addParams [Decl]
ds
NonRecursive Decl
d -> Decl -> DeclGroup
NonRecursive forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. AddParams t => t -> RewM t
addParams Decl
d
instance AddParams Decl where
addParams :: Decl -> RewM Decl
addParams Decl
d =
case Decl -> DeclDef
dDefinition Decl
d of
DeclDef
DPrim -> BIWhat -> RewM Decl
bad BIWhat
BIPrimitive
DForeign {} -> BIWhat -> RewM Decl
bad BIWhat
BIForeign
DExpr Expr
e ->
do (TypeParams
tps,[Prop]
cs) <- (Name -> TPFlavor) -> RewM (TypeParams, [Prop])
newTypeParams Name -> TPFlavor
TPSchemaParam
(ValParams
vps,[(Name, Prop)]
bs) <- TypeParams -> RewM (ValParams, [(Name, Prop)])
newValParams TypeParams
tps
let s :: Schema
s = Decl -> Schema
dSignature Decl
d
Prop
ty1 <- forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (Schema -> Prop
sType Schema
s)
[Prop]
ps1 <- forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps (Schema -> [Prop]
sProps Schema
s)
let ty2 :: Prop
ty2 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Prop -> Prop
tFun Prop
ty1 (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Name, Prop)]
bs)
Expr
e1 <- forall t. RewVal t => TypeParams -> Int -> ValParams -> t -> RewM t
rewValM TypeParams
tps (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Prop]
cs) ValParams
vps Expr
e
let ([TParam]
das,Expr
e2) = forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe (TParam, Expr)
splitTAbs Expr
e1
([Prop]
dcs,Expr
e3) = forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe (Prop, Expr)
splitProofAbs Expr
e2
e4 :: Expr
e4 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Prop -> Expr -> Expr
EAbs) Expr
e3 [(Name, Prop)]
bs
e5 :: Expr
e5 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Expr -> Expr
EProofAbs Expr
e4 ([Prop]
cs forall a. [a] -> [a] -> [a]
++ [Prop]
dcs)
e6 :: Expr
e6 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Expr -> Expr
ETAbs Expr
e5 (forall decl use. Params decl use -> [decl]
pDecl TypeParams
tps forall a. [a] -> [a] -> [a]
++ [TParam]
das)
s1 :: Schema
s1 = Forall
{ sVars :: [TParam]
sVars = forall decl use. Params decl use -> [decl]
pDecl TypeParams
tps forall a. [a] -> [a] -> [a]
++ Schema -> [TParam]
sVars Schema
s
, sProps :: [Prop]
sProps = [Prop]
cs forall a. [a] -> [a] -> [a]
++ [Prop]
ps1
, sType :: Prop
sType = Prop
ty2
}
forall (f :: * -> *) a. Applicative f => a -> f a
pure Decl
d { dDefinition :: DeclDef
dDefinition = Expr -> DeclDef
DExpr Expr
e6
, dSignature :: Schema
dSignature = Schema
s1
}
where
bad :: BIWhat -> RewM Decl
bad BIWhat
w =
do Error -> RewM ()
recordError (BadBacktickInstance -> Error
FunctorInstanceBadBacktick ([(BIWhat, Name)] -> BadBacktickInstance
BINested [(BIWhat
w,Decl -> Name
dName Decl
d)]))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Decl
d
data Params decl use = Params
{ forall decl use. Params decl use -> [decl]
pDecl :: [decl]
, forall decl use. Params decl use -> [use]
pUse :: [use]
, forall decl use. Params decl use -> Map decl use
pSubst :: Map decl use
}
noParams :: Params decl use
noParams :: forall decl use. Params decl use
noParams = Params
{ pDecl :: [decl]
pDecl = []
, pUse :: [use]
pUse = []
, pSubst :: Map decl use
pSubst = forall k a. Map k a
Map.empty
}
qualLabel :: Maybe ModName -> Ident -> Ident
qualLabel :: Maybe ModName -> Ident -> Ident
qualLabel Maybe ModName
mb Ident
i =
case Maybe ModName
mb of
Maybe ModName
Nothing -> Ident
i
Just ModName
mn ->
let txt :: Text
txt = Text -> [Text] -> Text
Text.intercalate Text
"'" (ModName -> [Text]
modNameChunksText ModName
mn forall a. [a] -> [a] -> [a]
++ [Ident -> Text
identText Ident
i])
in Text -> Ident
mkIdent Text
txt
type TypeParams = Params TParam Type
type ValParams = Params Name Expr
newTypeParams :: (Name -> TPFlavor) -> RewM (TypeParams,[Prop])
newTypeParams :: (Name -> TPFlavor) -> RewM (TypeParams, [Prop])
newTypeParams Name -> TPFlavor
flav =
do RO
ro <- forall (m :: * -> *) i. ReaderM m i => m i
ask
let newFlaf :: Maybe ModName -> Name -> TPFlavor
newFlaf Maybe ModName
q = Name -> TPFlavor
flav forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ident -> Ident) -> Name -> Name
mapNameIdent (Maybe ModName -> Ident -> Ident
qualLabel Maybe ModName
q)
[TParam]
as <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (RO -> [MBQual TParam]
tparams RO
ro) \(Maybe ModName
q,TParam
a) -> (Name -> TPFlavor) -> TParam -> InferM TParam
TC.freshTParam (Maybe ModName -> Name -> TPFlavor
newFlaf Maybe ModName
q) TParam
a)
let bad :: [Ident]
bad = [ Ident
x
| Ident
x : Ident
_ : [Ident]
_ <- forall a. Eq a => [a] -> [[a]]
group (forall a. Ord a => [a] -> [a]
sort (forall a b. (a -> b) -> [a] -> [b]
map Name -> Ident
nameIdent (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TParam -> Maybe Name
tpName [TParam]
as)))
]
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Ident]
bad \Ident
i ->
Error -> RewM ()
recordError (BadBacktickInstance -> Error
FunctorInstanceBadBacktick (Ident -> BadBacktickInstance
BIMultipleParams Ident
i))
let ts :: [Prop]
ts = forall a b. (a -> b) -> [a] -> [b]
map (TVar -> Prop
TVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> TVar
TVBound) [TParam]
as
su :: Map TParam Prop
su = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd (RO -> [MBQual TParam]
tparams RO
ro)) [Prop]
ts)
ps :: TypeParams
ps = Params { pDecl :: [TParam]
pDecl = [TParam]
as, pUse :: [Prop]
pUse = [Prop]
ts, pSubst :: Map TParam Prop
pSubst = Map TParam Prop
su }
[Prop]
cs <- forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
ps (RO -> [Prop]
constraints RO
ro)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeParams
ps,[Prop]
cs)
newValParams :: TypeParams -> RewM (ValParams, [(Name,Type)])
newValParams :: TypeParams -> RewM (ValParams, [(Name, Prop)])
newValParams TypeParams
tps =
do RO
ro <- forall (m :: * -> *) i. ReaderM m i => m i
ask
let vps :: Map (MBQual Name) Prop
vps = RO -> Map (MBQual Name) Prop
vparams RO
ro
if forall k a. Map k a -> Bool
Map.null Map (MBQual Name) Prop
vps
then forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall decl use. Params decl use
noParams, [])
else do [(Name, Ident, Prop)]
xts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall k a. Map k a -> [(k, a)]
Map.toList Map (MBQual Name) Prop
vps) \((Maybe ModName
q,Name
x),Prop
t) ->
do Prop
t1 <- forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
tps Prop
t
let l :: Ident
l = Maybe ModName -> Ident -> Ident
qualLabel Maybe ModName
q (Name -> Ident
nameIdent Name
x)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name
x, Ident
l, Prop
t1)
let ([Name]
xs,[Ident]
ls,[Prop]
ts) = forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 [(Name, Ident, Prop)]
xts
fs :: [(Ident, Prop)]
fs = forall a b. [a] -> [b] -> [(a, b)]
zip [Ident]
ls [Prop]
ts
sel :: Ident -> Selector
sel Ident
l = Ident -> Maybe [Ident] -> Selector
RecordSel Ident
l (forall a. a -> Maybe a
Just [Ident]
ls)
Prop
t <- case forall a b.
(Show a, Ord a) =>
[(a, b)] -> Either (a, b) (RecordMap a b)
recordFromFieldsErr [(Ident, Prop)]
fs of
Right RecordMap Ident Prop
ok -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (RecordMap Ident Prop -> Prop
TRec RecordMap Ident Prop
ok)
Left (Ident
x,Prop
_) ->
do Error -> RewM ()
recordError (BadBacktickInstance -> Error
FunctorInstanceBadBacktick
(Ident -> BadBacktickInstance
BIMultipleParams Ident
x))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RecordMap Ident Prop -> Prop
TRec (forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields [(Ident, Prop)]
fs))
Name
r <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift (Namespace -> Ident -> InferM Name
TC.newLocalName Namespace
NSValue (Text -> Ident
mkIdent Text
"params"))
let e :: Expr
e = Name -> Expr
EVar Name
r
forall (f :: * -> *) a. Applicative f => a -> f a
pure
( Params
{ pDecl :: [Name]
pDecl = [Name
r]
, pUse :: [Expr]
pUse = [Expr
e]
, pSubst :: Map Name Expr
pSubst = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Name
x,Expr -> Selector -> Expr
ESel Expr
e (Ident -> Selector
sel Ident
l))
| (Name
x,Ident
l) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
xs [Ident]
ls ]
}
, [ (Name
r,Prop
t) ]
)
liftRew ::
((?isOurs :: Name -> Bool, ?newNewtypes :: Map Name Newtype) => a) ->
RewM a
liftRew :: forall a.
((?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => a)
-> RewM a
liftRew (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => a
x =
do RO
ro <- forall (m :: * -> *) i. ReaderM m i => m i
ask
let ?isOurs = RO -> Name -> Bool
isOurs RO
ro
?newNewtypes = RO -> Map Name Newtype
newNewtypes RO
ro
forall (f :: * -> *) a. Applicative f => a -> f a
pure (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => a
x
rewTypeM :: RewType t => TypeParams -> t -> RewM t
rewTypeM :: forall t. RewType t => TypeParams -> t -> RewM t
rewTypeM TypeParams
ps t
x =
do let ?tparams = TypeParams
ps
forall a.
((?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => a)
-> RewM a
liftRew forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure t
x
rewValM :: RewVal t => TypeParams -> Int -> ValParams -> t -> RewM t
rewValM :: forall t. RewVal t => TypeParams -> Int -> ValParams -> t -> RewM t
rewValM TypeParams
ts Int
cs ValParams
vs t
x =
do let ?tparams = TypeParams
ts
?cparams = Int
cs
?vparams = ValParams
vs
forall a.
((?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => a)
-> RewM a
liftRew forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure t
x
class RewType t where
rewType ::
( ?isOurs :: Name -> Bool
, ?newNewtypes :: Map Name Newtype
, ?tparams :: TypeParams
) => t -> t
instance RewType Type where
rewType :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
Prop -> Prop
rewType Prop
ty =
case Prop
ty of
TCon TCon
tc [Prop]
ts
| TC (TCAbstract (UserTC Name
x Kind
_)) <- TCon
tc
, ?isOurs::Name -> Bool
?isOurs Name
x -> TCon -> [Prop] -> Prop
TCon TCon
tc (forall decl use. Params decl use -> [use]
pUse ?tparams::TypeParams
?tparams forall a. [a] -> [a] -> [a]
++ forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts)
| Bool
otherwise -> TCon -> [Prop] -> Prop
TCon TCon
tc (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts)
TVar TVar
x ->
case TVar
x of
TVBound TParam
x' ->
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TParam
x' (forall decl use. Params decl use -> Map decl use
pSubst ?tparams::TypeParams
?tparams) of
Just Prop
t -> Prop
t
Maybe Prop
Nothing -> Prop
ty
TVFree {} -> forall a. HasCallStack => String -> [String] -> a
panic String
"rawType" [String
"Free unification variable"]
TUser Name
f [Prop]
ts Prop
t
| ?isOurs::Name -> Bool
?isOurs Name
f -> Name -> [Prop] -> Prop -> Prop
TUser Name
f (forall decl use. Params decl use -> [use]
pUse ?tparams::TypeParams
?tparams forall a. [a] -> [a] -> [a]
++ forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts) (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType Prop
t)
| Bool
otherwise -> Name -> [Prop] -> Prop -> Prop
TUser Name
f (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts) (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType Prop
t)
TRec RecordMap Ident Prop
fs -> RecordMap Ident Prop -> Prop
TRec (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType RecordMap Ident Prop
fs)
TNewtype Newtype
tdef [Prop]
ts
| ?isOurs::Name -> Bool
?isOurs Name
nm -> Newtype -> [Prop] -> Prop
TNewtype Newtype
tdef' (forall decl use. Params decl use -> [use]
pUse ?tparams::TypeParams
?tparams forall a. [a] -> [a] -> [a]
++ forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts)
| Bool
otherwise -> Newtype -> [Prop] -> Prop
TNewtype Newtype
tdef (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts)
where
nm :: Name
nm = Newtype -> Name
ntName Newtype
tdef
tdef' :: Newtype
tdef' = case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
nm ?newNewtypes::Map Name Newtype
?newNewtypes of
Just Newtype
yes -> Newtype
yes
Maybe Newtype
Nothing -> forall a. HasCallStack => String -> [String] -> a
panic String
"rewType" [ String
"Missing recursive newtype"
, forall a. Show a => a -> String
show (forall a. PP a => a -> Doc
pp Name
nm) ]
instance RewType a => RewType [a] where
rewType :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
[a] -> [a]
rewType = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType
instance RewType b => RewType (RecordMap a b) where
rewType :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
RecordMap a b -> RecordMap a b
rewType = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType
instance RewType Schema where
rewType :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
Schema -> Schema
rewType Schema
sch =
Forall { sVars :: [TParam]
sVars = Schema -> [TParam]
sVars Schema
sch
, sProps :: [Prop]
sProps = forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType (Schema -> [Prop]
sProps Schema
sch)
, sType :: Prop
sType = forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType (Schema -> Prop
sType Schema
sch)
}
class RewVal t where
rew ::
( ?isOurs :: Name -> Bool
, ?newNewtypes :: Map Name Newtype
, ?tparams :: TypeParams
, ?cparams :: Int
, ?vparams :: ValParams
) => t -> t
instance RewVal a => RewVal [a] where
rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
[a] -> [a]
rew = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew
instance RewVal b => RewVal (RecordMap a b) where
rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
RecordMap a b -> RecordMap a b
rew = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew
instance RewVal Expr where
rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
Expr -> Expr
rew Expr
expr =
case Expr
expr of
EList [Expr]
es Prop
t -> [Expr] -> Prop -> Expr
EList (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew [Expr]
es) (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType Prop
t)
ETuple [Expr]
es -> [Expr] -> Expr
ETuple (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew [Expr]
es)
ERec RecordMap Ident Expr
fs -> RecordMap Ident Expr -> Expr
ERec (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew RecordMap Ident Expr
fs)
ESel Expr
e Selector
l -> Expr -> Selector -> Expr
ESel (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e) Selector
l
ESet Prop
t Expr
e1 Selector
s Expr
e2 -> Prop -> Expr -> Selector -> Expr -> Expr
ESet (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType Prop
t) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e1) Selector
s (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e2)
EIf Expr
e1 Expr
e2 Expr
e3 -> Expr -> Expr -> Expr -> Expr
EIf (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e1) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e2) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e3)
EComp Prop
t1 Prop
t2 Expr
e [[Match]]
mss -> Prop -> Prop -> Expr -> [[Match]] -> Expr
EComp (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType Prop
t1) (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType Prop
t2) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew [[Match]]
mss)
EVar Name
x -> forall {decl}.
(?tparams::TypeParams, ?isOurs::Name -> Bool,
?vparams::Params decl Expr, ?newNewtypes::Map Name Newtype,
?cparams::Int) =>
Expr -> Expr
tryVarApp
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x (forall decl use. Params decl use -> Map decl use
pSubst ?vparams::ValParams
?vparams) of
Just Expr
p -> Expr
p
Maybe Expr
Nothing -> Expr
expr
ETApp Expr
e Prop
t -> forall {decl}.
(?tparams::TypeParams, ?isOurs::Name -> Bool,
?vparams::Params decl Expr, ?newNewtypes::Map Name Newtype,
?cparams::Int) =>
Expr -> Expr
tryVarApp (Expr -> Prop -> Expr
ETApp (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e) (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType Prop
t))
EProofApp Expr
e -> forall {decl}.
(?tparams::TypeParams, ?isOurs::Name -> Bool,
?vparams::Params decl Expr, ?newNewtypes::Map Name Newtype,
?cparams::Int) =>
Expr -> Expr
tryVarApp (Expr -> Expr
EProofApp (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e))
EApp Expr
e1 Expr
e2 -> Expr -> Expr -> Expr
EApp (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e1) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e2)
ETAbs TParam
a Expr
e -> TParam -> Expr -> Expr
ETAbs TParam
a (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e)
EAbs Name
x Prop
t Expr
e -> Name -> Prop -> Expr -> Expr
EAbs Name
x (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType Prop
t) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e)
ELocated Range
r Expr
e -> Range -> Expr -> Expr
ELocated Range
r (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e)
EProofAbs Prop
p Expr
e -> Prop -> Expr -> Expr
EProofAbs (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType Prop
p) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e)
EWhere Expr
e [DeclGroup]
ds -> Expr -> [DeclGroup] -> Expr
EWhere (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew [DeclGroup]
ds)
EPropGuards [([Prop], Expr)]
gs Prop
t -> [([Prop], Expr)] -> Prop -> Expr
EPropGuards [([Prop], Expr)]
gs' (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType Prop
t)
where gs' :: [([Prop], Expr)]
gs' = [ (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Prop]
p, forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e) | ([Prop]
p,Expr
e) <- [([Prop], Expr)]
gs ]
where
tryVarApp :: Expr -> Expr
tryVarApp Expr
orElse =
case Expr -> (Expr, [Prop], Int)
splitExprInst Expr
expr of
(EVar Name
x, [Prop]
ts, Int
cs) | ?isOurs::Name -> Bool
?isOurs Name
x ->
let ets :: Expr
ets = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Prop -> Expr
ETApp (Name -> Expr
EVar Name
x) (forall decl use. Params decl use -> [use]
pUse ?tparams::TypeParams
?tparams forall a. [a] -> [a] -> [a]
++ forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType [Prop]
ts)
eps :: Expr
eps = forall a. (a -> a) -> a -> [a]
iterate Expr -> Expr
EProofApp Expr
ets forall a. [a] -> Int -> a
!! (?cparams::Int
?cparams forall a. Num a => a -> a -> a
+ Int
cs)
evs :: Expr
evs = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Expr -> Expr
EApp Expr
eps (forall decl use. Params decl use -> [use]
pUse ?vparams::Params decl Expr
?vparams)
in Expr
evs
(Expr, [Prop], Int)
_ -> Expr
orElse
instance RewVal DeclGroup where
rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
DeclGroup -> DeclGroup
rew DeclGroup
dg =
case DeclGroup
dg of
Recursive [Decl]
ds -> [Decl] -> DeclGroup
Recursive (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew [Decl]
ds)
NonRecursive Decl
d -> Decl -> DeclGroup
NonRecursive (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Decl
d)
instance RewVal Decl where
rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
Decl -> Decl
rew Decl
d = Decl
d { dDefinition :: DeclDef
dDefinition = forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew (Decl -> DeclDef
dDefinition Decl
d)
, dSignature :: Schema
dSignature = forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType (Decl -> Schema
dSignature Decl
d)
}
instance RewVal DeclDef where
rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
DeclDef -> DeclDef
rew DeclDef
def =
case DeclDef
def of
DeclDef
DPrim -> DeclDef
def
DForeign {} -> DeclDef
def
DExpr Expr
e -> Expr -> DeclDef
DExpr (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e)
instance RewVal Match where
rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
Match -> Match
rew Match
ma =
case Match
ma of
From Name
x Prop
t1 Prop
t2 Expr
e -> Name -> Prop -> Prop -> Expr -> Match
From Name
x (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType Prop
t1) (forall t.
(RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams) =>
t -> t
rewType Prop
t2) (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Expr
e)
Let Decl
d -> Decl -> Match
Let (forall t.
(RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
t -> t
rew Decl
d)