{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module Cryptol.Transform.Specialize
where
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.TypeMap
import Cryptol.TypeCheck.Subst
import qualified Cryptol.ModuleSystem as M
import qualified Cryptol.ModuleSystem.Env as M
import qualified Cryptol.ModuleSystem.Monad as M
import Cryptol.ModuleSystem.Name
import Cryptol.Utils.Ident(OrigName(..))
import Cryptol.Eval (checkProp)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (catMaybes)
import qualified Data.List as List
import MonadLib hiding (mapM)
import Cryptol.ModuleSystem.Base (getPrimMap)
type SpecCache = Map Name (Decl, TypesMap (Name, Maybe Decl))
type SpecT m a = StateT SpecCache (M.ModuleT m) a
type SpecM a = SpecT IO a
runSpecT :: SpecCache -> SpecT m a -> M.ModuleT m (a, SpecCache)
runSpecT :: forall (m :: * -> *) a.
SpecCache -> SpecT m a -> ModuleT m (a, SpecCache)
runSpecT SpecCache
s SpecT m a
m = forall i (m :: * -> *) a. i -> StateT i m a -> m (a, i)
runStateT SpecCache
s SpecT m a
m
liftSpecT :: Monad m => M.ModuleT m a -> SpecT m a
liftSpecT :: forall (m :: * -> *) a. Monad m => ModuleT m a -> SpecT m a
liftSpecT ModuleT m a
m = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift ModuleT m a
m
getSpecCache :: Monad m => SpecT m SpecCache
getSpecCache :: forall (m :: * -> *). Monad m => SpecT m SpecCache
getSpecCache = forall (m :: * -> *) i. StateM m i => m i
get
setSpecCache :: Monad m => SpecCache -> SpecT m ()
setSpecCache :: forall (m :: * -> *). Monad m => SpecCache -> SpecT m ()
setSpecCache = forall (m :: * -> *) i. StateM m i => i -> m ()
set
modifySpecCache :: Monad m => (SpecCache -> SpecCache) -> SpecT m ()
modifySpecCache :: forall (m :: * -> *).
Monad m =>
(SpecCache -> SpecCache) -> SpecT m ()
modifySpecCache = forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
modify
modify :: StateM m s => (s -> s) -> m ()
modify :: forall (m :: * -> *) s. StateM m s => (s -> s) -> m ()
modify s -> s
f = forall (m :: * -> *) i. StateM m i => m i
get forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall (m :: * -> *) i. StateM m i => i -> m ()
set forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> s
f)
specialize :: Expr -> M.ModuleCmd Expr
specialize :: Expr -> ModuleCmd Expr
specialize Expr
expr ModuleInput IO
minp = forall {a}.
SpecT IO a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
run forall a b. (a -> b) -> a -> b
$ do
let extDgs :: [DeclGroup]
extDgs = ModuleEnv -> [DeclGroup]
allDeclGroups (forall (m :: * -> *). ModuleInput m -> ModuleEnv
M.minpModuleEnv ModuleInput IO
minp)
let ([TParam]
tparams, Expr
expr') = Expr -> ([TParam], Expr)
destETAbs Expr
expr
Expr
spec' <- Expr -> [DeclGroup] -> SpecT IO Expr
specializeEWhere Expr
expr' [DeclGroup]
extDgs
forall (m :: * -> *) a. Monad m => a -> m a
return (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Expr -> Expr
ETAbs Expr
spec' [TParam]
tparams)
where
run :: SpecT IO a
-> IO (Either ModuleError (a, ModuleEnv), [ModuleWarning])
run = forall (m :: * -> *) a.
Monad m =>
ModuleInput m
-> ModuleT m a
-> m (Either ModuleError (a, ModuleEnv), [ModuleWarning])
M.runModuleT ModuleInput IO
minp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a.
SpecCache -> SpecT m a -> ModuleT m (a, SpecCache)
runSpecT forall k a. Map k a
Map.empty
specializeExpr :: Expr -> SpecM Expr
specializeExpr :: Expr -> SpecT IO Expr
specializeExpr Expr
expr =
case Expr
expr of
ELocated Range
r Expr
e -> Range -> Expr -> Expr
ELocated Range
r forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> SpecT IO Expr
specializeExpr Expr
e
EList [Expr]
es Type
t -> [Expr] -> Type -> Expr
EList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr -> SpecT IO Expr
specializeExpr [Expr]
es forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
t
ETuple [Expr]
es -> [Expr] -> Expr
ETuple forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr -> SpecT IO Expr
specializeExpr [Expr]
es
ERec RecordMap Ident Expr
fs -> RecordMap Ident Expr -> Expr
ERec forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr -> SpecT IO Expr
specializeExpr RecordMap Ident Expr
fs
ESel Expr
e Selector
s -> Expr -> Selector -> Expr
ESel forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> SpecT IO Expr
specializeExpr Expr
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Selector
s
ESet Type
ty Expr
e Selector
s Expr
v -> Type -> Expr -> Selector -> Expr -> Expr
ESet Type
ty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> SpecT IO Expr
specializeExpr Expr
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Selector
s forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> SpecT IO Expr
specializeExpr Expr
v
EIf Expr
e1 Expr
e2 Expr
e3 -> Expr -> Expr -> Expr -> Expr
EIf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> SpecT IO Expr
specializeExpr Expr
e1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> SpecT IO Expr
specializeExpr Expr
e2 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> SpecT IO Expr
specializeExpr Expr
e3
EComp Type
len Type
t Expr
e [[Match]]
mss -> Type -> Type -> Expr -> [[Match]] -> Expr
EComp Type
len Type
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> SpecT IO Expr
specializeExpr Expr
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Match -> SpecM Match
specializeMatch) [[Match]]
mss
EVar {} -> Expr -> SpecT IO Expr
specializeConst Expr
expr
ETAbs TParam
t Expr
e -> do
SpecCache
cache <- forall (m :: * -> *). Monad m => SpecT m SpecCache
getSpecCache
forall (m :: * -> *). Monad m => SpecCache -> SpecT m ()
setSpecCache forall k a. Map k a
Map.empty
Expr
e' <- Expr -> SpecT IO Expr
specializeExpr Expr
e
forall (m :: * -> *). Monad m => SpecCache -> SpecT m ()
setSpecCache SpecCache
cache
forall (m :: * -> *) a. Monad m => a -> m a
return (TParam -> Expr -> Expr
ETAbs TParam
t Expr
e')
ETApp {} -> Expr -> SpecT IO Expr
specializeConst Expr
expr
EApp Expr
e1 Expr
e2 -> Expr -> Expr -> Expr
EApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> SpecT IO Expr
specializeExpr Expr
e1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> SpecT IO Expr
specializeExpr Expr
e2
EAbs Name
qn Type
t Expr
e -> Name -> Type -> Expr -> Expr
EAbs Name
qn Type
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> SpecT IO Expr
specializeExpr Expr
e
EProofAbs Type
p Expr
e -> Type -> Expr -> Expr
EProofAbs Type
p forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> SpecT IO Expr
specializeExpr Expr
e
EProofApp {} -> Expr -> SpecT IO Expr
specializeConst Expr
expr
EWhere Expr
e [DeclGroup]
dgs -> Expr -> [DeclGroup] -> SpecT IO Expr
specializeEWhere Expr
e [DeclGroup]
dgs
EPropGuards [([Type], Expr)]
guards Type
ty ->
case forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
checkProp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [([Type], Expr)]
guards of
Just ([Type]
_, Expr
e) -> Expr -> SpecT IO Expr
specializeExpr Expr
e
Maybe ([Type], Expr)
Nothing -> do
PrimMap
pm <- forall (m :: * -> *) a. Monad m => ModuleT m a -> SpecT m a
liftSpecT ModuleM PrimMap
getPrimMap
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ PrimMap -> Type -> String -> Expr
eError PrimMap
pm Type
ty String
"no constraint guard was satisfied"
specializeMatch :: Match -> SpecM Match
specializeMatch :: Match -> SpecM Match
specializeMatch (From Name
qn Type
l Type
t Expr
e) = Name -> Type -> Type -> Expr -> Match
From Name
qn Type
l Type
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> SpecT IO Expr
specializeExpr Expr
e
specializeMatch (Let Decl
decl)
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Schema -> [TParam]
sVars (Decl -> Schema
dSignature Decl
decl)) = forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> Match
Let Decl
decl)
| Bool
otherwise = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"unimplemented: specializeMatch Let unimplemented"
withDeclGroups :: [DeclGroup] -> SpecM a
-> SpecM (a, [DeclGroup], Map Name (TypesMap Name))
withDeclGroups :: forall a.
[DeclGroup]
-> SpecM a -> SpecM (a, [DeclGroup], Map Name (TypesMap Name))
withDeclGroups [DeclGroup]
dgs SpecM a
action = do
SpecCache
origCache <- forall (m :: * -> *). Monad m => SpecT m SpecCache
getSpecCache
let decls :: [Decl]
decls = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DeclGroup -> [Decl]
groupDecls [DeclGroup]
dgs
let newCache :: Map Name (Decl, List TypeMap a)
newCache = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Decl -> Name
dName Decl
d, (Decl
d, forall (m :: * -> *) k a. TrieMap m k => m a
emptyTM)) | Decl
d <- [Decl]
decls ]
let savedCache :: SpecCache
savedCache = forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection SpecCache
origCache forall {a}. Map Name (Decl, List TypeMap a)
newCache
forall (m :: * -> *). Monad m => SpecCache -> SpecT m ()
setSpecCache (forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union forall {a}. Map Name (Decl, List TypeMap a)
newCache SpecCache
origCache)
a
result <- SpecM a
action
let splitDecl :: Decl -> SpecM [Decl]
splitDecl :: Decl -> SpecM [Decl]
splitDecl Decl
d = do
~(Just (Decl
_, TypesMap (Name, Maybe Decl)
tm)) <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Decl -> Name
dName Decl
d) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Monad m => SpecT m SpecCache
getSpecCache
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [Maybe a] -> [a]
catMaybes forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) k a. TrieMap m k => m a -> [(k, a)]
toListTM TypesMap (Name, Maybe Decl)
tm)
let splitDeclGroup :: DeclGroup -> SpecM [DeclGroup]
splitDeclGroup :: DeclGroup -> SpecM [DeclGroup]
splitDeclGroup (Recursive [Decl]
ds) = do
[Decl]
ds' <- forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Decl -> SpecM [Decl]
splitDecl [Decl]
ds
if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Decl]
ds'
then forall (m :: * -> *) a. Monad m => a -> m a
return []
else forall (m :: * -> *) a. Monad m => a -> m a
return [[Decl] -> DeclGroup
Recursive [Decl]
ds']
splitDeclGroup (NonRecursive Decl
d) = forall a b. (a -> b) -> [a] -> [b]
map Decl -> DeclGroup
NonRecursive forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Decl -> SpecM [Decl]
splitDecl Decl
d
[DeclGroup]
dgs' <- forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse DeclGroup -> SpecM [DeclGroup]
splitDeclGroup [DeclGroup]
dgs
SpecCache
newCache' <- forall a b c. (a -> b -> c) -> b -> a -> c
flip forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection forall {a}. Map Name (Decl, List TypeMap a)
newCache forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Monad m => SpecT m SpecCache
getSpecCache
let nameTable :: Map Name (TypesMap Name)
nameTable = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) SpecCache
newCache'
forall (m :: * -> *).
Monad m =>
(SpecCache -> SpecCache) -> SpecT m ()
modifySpecCache (forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union SpecCache
savedCache forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.difference forall {a}. Map Name (Decl, List TypeMap a)
newCache)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
result, [DeclGroup]
dgs', Map Name (TypesMap Name)
nameTable)
specializeEWhere :: Expr -> [DeclGroup] -> SpecM Expr
specializeEWhere :: Expr -> [DeclGroup] -> SpecT IO Expr
specializeEWhere Expr
e [DeclGroup]
dgs = do
(Expr
e', [DeclGroup]
dgs', Map Name (TypesMap Name)
_) <- forall a.
[DeclGroup]
-> SpecM a -> SpecM (a, [DeclGroup], Map Name (TypesMap Name))
withDeclGroups [DeclGroup]
dgs (Expr -> SpecT IO Expr
specializeExpr Expr
e)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DeclGroup]
dgs'
then Expr
e'
else Expr -> [DeclGroup] -> Expr
EWhere Expr
e' [DeclGroup]
dgs'
specializeDeclGroups :: [DeclGroup] -> SpecM ([DeclGroup], Map Name (TypesMap Name))
specializeDeclGroups :: [DeclGroup] -> SpecM ([DeclGroup], Map Name (TypesMap Name))
specializeDeclGroups [DeclGroup]
dgs = do
let decls :: [Decl]
decls = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DeclGroup -> [Decl]
groupDecls [DeclGroup]
dgs
let isMonoType :: Schema -> Bool
isMonoType Schema
s = forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Schema -> [TParam]
sVars Schema
s) Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Schema -> [Type]
sProps Schema
s)
let monos :: [Expr]
monos = [ Name -> Expr
EVar (Decl -> Name
dName Decl
d) | Decl
d <- [Decl]
decls, Schema -> Bool
isMonoType (Decl -> Schema
dSignature Decl
d) ]
([Expr]
_, [DeclGroup]
dgs', Map Name (TypesMap Name)
names) <- forall a.
[DeclGroup]
-> SpecM a -> SpecM (a, [DeclGroup], Map Name (TypesMap Name))
withDeclGroups [DeclGroup]
dgs forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Expr -> SpecT IO Expr
specializeExpr [Expr]
monos
forall (m :: * -> *) a. Monad m => a -> m a
return ([DeclGroup]
dgs', Map Name (TypesMap Name)
names)
specializeConst :: Expr -> SpecM Expr
specializeConst :: Expr -> SpecT IO Expr
specializeConst Expr
e0 = do
let (Expr
e1, Int
n) = Expr -> (Expr, Int)
destEProofApps Expr
e0
let (Expr
e2, [Type]
ts) = Expr -> (Expr, [Type])
destETApps Expr
e1
case Expr
e2 of
EVar Name
qname ->
do SpecCache
cache <- forall (m :: * -> *). Monad m => SpecT m SpecCache
getSpecCache
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
qname SpecCache
cache of
Maybe (Decl, TypesMap (Name, Maybe Decl))
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e0
Just (Decl
decl, TypesMap (Name, Maybe Decl)
tm) ->
case forall (m :: * -> *) k a. TrieMap m k => k -> m a -> Maybe a
lookupTM [Type]
ts TypesMap (Name, Maybe Decl)
tm of
Just (Name
qname', Maybe Decl
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Expr
EVar Name
qname')
Maybe (Name, Maybe Decl)
Nothing -> do
Name
qname' <- Name -> [Type] -> SpecM Name
freshName Name
qname [Type]
ts
Schema
sig' <- [Type] -> Int -> Schema -> SpecM Schema
instantiateSchema [Type]
ts Int
n (Decl -> Schema
dSignature Decl
decl)
forall (m :: * -> *).
Monad m =>
(SpecCache -> SpecCache) -> SpecT m ()
modifySpecCache (forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (m :: * -> *) k a. TrieMap m k => k -> a -> m a -> m a
insertTM [Type]
ts (Name
qname', forall a. Maybe a
Nothing))) Name
qname)
DeclDef
rhs' <- case Decl -> DeclDef
dDefinition Decl
decl of
DExpr Expr
e -> do Expr
e' <- Expr -> SpecT IO Expr
specializeExpr forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Type] -> Int -> Expr -> SpecT IO Expr
instantiateExpr [Type]
ts Int
n Expr
e
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> DeclDef
DExpr Expr
e')
DeclDef
DPrim -> forall (m :: * -> *) a. Monad m => a -> m a
return DeclDef
DPrim
DForeign FFIFunType
t -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FFIFunType -> DeclDef
DForeign FFIFunType
t
let decl' :: Decl
decl' = Decl
decl { dName :: Name
dName = Name
qname', dSignature :: Schema
dSignature = Schema
sig', dDefinition :: DeclDef
dDefinition = DeclDef
rhs' }
forall (m :: * -> *).
Monad m =>
(SpecCache -> SpecCache) -> SpecT m ()
modifySpecCache (forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (m :: * -> *) k a. TrieMap m k => k -> a -> m a -> m a
insertTM [Type]
ts (Name
qname', forall a. a -> Maybe a
Just Decl
decl'))) Name
qname)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Expr
EVar Name
qname')
Expr
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e0
destEProofApps :: Expr -> (Expr, Int)
destEProofApps :: Expr -> (Expr, Int)
destEProofApps = forall {b}. Num b => b -> Expr -> (Expr, b)
go Int
0
where
go :: b -> Expr -> (Expr, b)
go b
n (EProofApp Expr
e) = b -> Expr -> (Expr, b)
go (b
n forall a. Num a => a -> a -> a
+ b
1) Expr
e
go b
n Expr
e = (Expr
e, b
n)
destETApps :: Expr -> (Expr, [Type])
destETApps :: Expr -> (Expr, [Type])
destETApps = [Type] -> Expr -> (Expr, [Type])
go []
where
go :: [Type] -> Expr -> (Expr, [Type])
go [Type]
ts (ETApp Expr
e Type
t) = [Type] -> Expr -> (Expr, [Type])
go (Type
t forall a. a -> [a] -> [a]
: [Type]
ts) Expr
e
go [Type]
ts Expr
e = (Expr
e, [Type]
ts)
destEProofAbs :: Expr -> ([Prop], Expr)
destEProofAbs :: Expr -> ([Type], Expr)
destEProofAbs = [Type] -> Expr -> ([Type], Expr)
go []
where
go :: [Type] -> Expr -> ([Type], Expr)
go [Type]
ps (EProofAbs Type
p Expr
e) = [Type] -> Expr -> ([Type], Expr)
go (Type
p forall a. a -> [a] -> [a]
: [Type]
ps) Expr
e
go [Type]
ps Expr
e = ([Type]
ps, Expr
e)
destETAbs :: Expr -> ([TParam], Expr)
destETAbs :: Expr -> ([TParam], Expr)
destETAbs = [TParam] -> Expr -> ([TParam], Expr)
go []
where
go :: [TParam] -> Expr -> ([TParam], Expr)
go [TParam]
ts (ETAbs TParam
t Expr
e) = [TParam] -> Expr -> ([TParam], Expr)
go (TParam
t forall a. a -> [a] -> [a]
: [TParam]
ts) Expr
e
go [TParam]
ts Expr
e = ([TParam]
ts, Expr
e)
freshName :: Name -> [Type] -> SpecM Name
freshName :: Name -> [Type] -> SpecM Name
freshName Name
n [Type]
_ =
case Name -> NameInfo
nameInfo Name
n of
GlobalName NameSource
s OrigName
og -> forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
liftSupply (Namespace
-> ModPath
-> NameSource
-> Ident
-> Maybe Fixity
-> Range
-> Supply
-> (Name, Supply)
mkDeclared Namespace
ns (OrigName -> ModPath
ogModule OrigName
og) NameSource
s Ident
ident Maybe Fixity
fx Range
loc)
LocalName {} -> forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
liftSupply (Namespace -> Ident -> Range -> Supply -> (Name, Supply)
mkLocal Namespace
ns Ident
ident Range
loc)
where
ns :: Namespace
ns = Name -> Namespace
nameNamespace Name
n
fx :: Maybe Fixity
fx = Name -> Maybe Fixity
nameFixity Name
n
ident :: Ident
ident = Name -> Ident
nameIdent Name
n
loc :: Range
loc = Name -> Range
nameLoc Name
n
instantiateSchema :: [Type] -> Int -> Schema -> SpecM Schema
instantiateSchema :: [Type] -> Int -> Schema -> SpecM Schema
instantiateSchema [Type]
ts Int
n (Forall [TParam]
params [Type]
props Type
ty)
| forall (t :: * -> *) a. Foldable t => t a -> Int
length [TParam]
params forall a. Eq a => a -> a -> Bool
/= forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"instantiateSchema: wrong number of type arguments"
| forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
props forall a. Eq a => a -> a -> Bool
/= Int
n = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"instantiateSchema: wrong number of prop arguments"
| Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [TParam] -> [Type] -> Type -> Schema
Forall [] [] (forall t. TVars t => Subst -> t -> t
apSubst Subst
sub Type
ty)
where sub :: Subst
sub = [(TParam, Type)] -> Subst
listParamSubst (forall a b. [a] -> [b] -> [(a, b)]
zip [TParam]
params [Type]
ts)
instantiateExpr :: [Type] -> Int -> Expr -> SpecM Expr
instantiateExpr :: [Type] -> Int -> Expr -> SpecT IO Expr
instantiateExpr [] Int
0 Expr
e = forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
instantiateExpr [] Int
n (EProofAbs Type
_ Expr
e) = [Type] -> Int -> Expr -> SpecT IO Expr
instantiateExpr [] (Int
n forall a. Num a => a -> a -> a
- Int
1) Expr
e
instantiateExpr (Type
t : [Type]
ts) Int
n (ETAbs TParam
param Expr
e) =
[Type] -> Int -> Expr -> SpecT IO Expr
instantiateExpr [Type]
ts Int
n (forall t. TVars t => Subst -> t -> t
apSubst (TParam -> Type -> Subst
singleTParamSubst TParam
param Type
t) Expr
e)
instantiateExpr [Type]
_ Int
_ Expr
_ = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"instantiateExpr: wrong number of type/proof arguments"
allDeclGroups :: M.ModuleEnv -> [DeclGroup]
allDeclGroups :: ModuleEnv -> [DeclGroup]
allDeclGroups =
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall mname. ModuleG mname -> [DeclGroup]
mDecls
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleEnv -> [Module]
M.loadedModules
traverseSnd :: Functor f => (b -> f c) -> (a, b) -> f (a, c)
traverseSnd :: forall (f :: * -> *) b c a.
Functor f =>
(b -> f c) -> (a, b) -> f (a, c)
traverseSnd b -> f c
f (a
x, b
y) = (,) a
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> f c
f b
y