-- | Transformed a parametrized module into an ordinary module
-- where everything is parameterized by the module's parameters.
-- Note that this reuses the names from the original parameterized module.
module Cryptol.Transform.AddModParams (addModParams) where

import           Data.Map ( Map )
import qualified Data.Map as Map
import           Data.Set ( Set )
import qualified Data.Set as Set
import           Data.Either(partitionEithers)
import           Data.List(find,sortBy)
import           Data.Ord(comparing)

import Cryptol.TypeCheck.AST
import Cryptol.Parser.Position(thing)
import Cryptol.ModuleSystem.Name(toParamInstName,asParamName,nameIdent
                                ,paramModRecParam)
import Cryptol.Utils.Ident(paramInstModName)
import Cryptol.Utils.RecordMap(recordFromFields)

{-
Note that we have to be careful when doing this transformation on
polyomorphic values.  In particular,


Consider type parameters AS, with constraints CS, and value
parameters (xs : TS).

    f : {as} PS => t
    f = f`{as} (<> ..)

    ~~>

    f : {AS ++ as} (CS ++ PS) => { TS } -> t
    f = /\ (AS ++ as) ->
        \\ (CS ++ PS) ->
        \r -> f`{AS ++ as} (<> ...) r

The tricky bit is that we can't just replace `f` with
a new version of `f` with some arguments, instead ew have
to modify the whole instantiation of `f` : f`{as} (<>...)

-}


addModParams :: Module -> Either [Name] Module
addModParams :: Module -> Either [Name] Module
addModParams Module
m =
  case Module -> Either [Name] Params
getParams Module
m of
    Left [Name]
errs -> [Name] -> Either [Name] Module
forall a b. a -> Either a b
Left [Name]
errs
    Right Params
ps ->
     let toInst :: Set Name
toInst = [Set Name] -> Set Name
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ( Map Name TySyn -> Set Name
forall k a. Map k a -> Set k
Map.keysSet (Module -> Map Name TySyn
mTySyns Module
m)
                             Set Name -> [Set Name] -> [Set Name]
forall a. a -> [a] -> [a]
: Map Name Newtype -> Set Name
forall k a. Map k a -> Set k
Map.keysSet (Module -> Map Name Newtype
mNewtypes Module
m)
                             Set Name -> [Set Name] -> [Set Name]
forall a. a -> [a] -> [a]
: (DeclGroup -> Set Name) -> [DeclGroup] -> [Set Name]
forall a b. (a -> b) -> [a] -> [b]
map DeclGroup -> Set Name
defs (Module -> [DeclGroup]
mDecls Module
m)
                             )
         inp :: (Set Name, Params)
inp = (Set Name
toInst, Params
ps { pTypeConstraints :: [Prop]
pTypeConstraints = (Set Name, Params) -> [Prop] -> [Prop]
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
inp (Params -> [Prop]
pTypeConstraints Params
ps) })

     in Module -> Either [Name] Module
forall a b. b -> Either a b
Right Module
m { mName :: ModName
mName = ModName -> ModName
paramInstModName (Module -> ModName
mName Module
m)
                , mTySyns :: Map Name TySyn
mTySyns = (Set Name, Params) -> Map Name TySyn -> Map Name TySyn
forall a.
(AddParams a, Inst a) =>
(Set Name, Params) -> Map Name a -> Map Name a
fixMap (Set Name, Params)
inp (Module -> Map Name TySyn
mTySyns Module
m)
                , mNewtypes :: Map Name Newtype
mNewtypes = (Set Name, Params) -> Map Name Newtype -> Map Name Newtype
forall a.
(AddParams a, Inst a) =>
(Set Name, Params) -> Map Name a -> Map Name a
fixMap (Set Name, Params)
inp (Module -> Map Name Newtype
mNewtypes Module
m)
                , mDecls :: [DeclGroup]
mDecls = (Set Name, Params) -> [DeclGroup] -> [DeclGroup]
forall a. (AddParams a, Inst a) => (Set Name, Params) -> a -> a
fixUp (Set Name, Params)
inp (Module -> [DeclGroup]
mDecls Module
m)
                , mParamTypes :: Map Name ModTParam
mParamTypes = Map Name ModTParam
forall k a. Map k a
Map.empty
                , mParamConstraints :: [Located Prop]
mParamConstraints = []
                , mParamFuns :: Map Name ModVParam
mParamFuns = Map Name ModVParam
forall k a. Map k a
Map.empty
                }

defs :: DeclGroup -> Set Name
defs :: DeclGroup -> Set Name
defs DeclGroup
dg =
  case DeclGroup
dg of
    Recursive [Decl]
ds -> [Name] -> Set Name
forall a. Ord a => [a] -> Set a
Set.fromList ((Decl -> Name) -> [Decl] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> Name
dName [Decl]
ds)
    NonRecursive Decl
d -> Name -> Set Name
forall a. a -> Set a
Set.singleton (Decl -> Name
dName Decl
d)

fixUp :: (AddParams a, Inst a) => Inp -> a -> a
fixUp :: (Set Name, Params) -> a -> a
fixUp (Set Name, Params)
i = Params -> a -> a
forall a. AddParams a => Params -> a -> a
addParams ((Set Name, Params) -> Params
forall a b. (a, b) -> b
snd (Set Name, Params)
i) (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set Name, Params) -> a -> a
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
i

fixMap :: (AddParams a, Inst a) => Inp -> Map Name a -> Map Name a
fixMap :: (Set Name, Params) -> Map Name a -> Map Name a
fixMap (Set Name, Params)
i Map Name a
m =
  [(Name, a)] -> Map Name a
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Name -> Name
toParamInstName Name
x, (Set Name, Params) -> a -> a
forall a. (AddParams a, Inst a) => (Set Name, Params) -> a -> a
fixUp (Set Name, Params)
i a
a) | (Name
x,a
a) <- Map Name a -> [(Name, a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Name a
m ]

--------------------------------------------------------------------------------

data Params = Params
  { Params -> [TParam]
pTypes            :: [TParam]
  , Params -> [Prop]
pTypeConstraints  :: [Prop]
  , Params -> [(Name, Prop)]
pFuns             :: [(Name,Type)]
  }


getParams :: Module -> Either [Name] Params
getParams :: Module -> Either [Name] Params
getParams Module
m
  | [Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
errs =
     let ps :: Params
ps = Params :: [TParam] -> [Prop] -> [(Name, Prop)] -> Params
Params { pTypes :: [TParam]
pTypes = (ModTParam -> TParam) -> [ModTParam] -> [TParam]
forall a b. (a -> b) -> [a] -> [b]
map ModTParam -> TParam
rnTP
                              ([ModTParam] -> [TParam]) -> [ModTParam] -> [TParam]
forall a b. (a -> b) -> a -> b
$ (ModTParam -> ModTParam -> Ordering) -> [ModTParam] -> [ModTParam]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ((ModTParam -> Int) -> ModTParam -> ModTParam -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing ModTParam -> Int
mtpNumber)
                              ([ModTParam] -> [ModTParam]) -> [ModTParam] -> [ModTParam]
forall a b. (a -> b) -> a -> b
$ Map Name ModTParam -> [ModTParam]
forall k a. Map k a -> [a]
Map.elems
                              (Map Name ModTParam -> [ModTParam])
-> Map Name ModTParam -> [ModTParam]
forall a b. (a -> b) -> a -> b
$ Module -> Map Name ModTParam
mParamTypes Module
m
                     , pTypeConstraints :: [Prop]
pTypeConstraints = (Located Prop -> Prop) -> [Located Prop] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Located Prop -> Prop
forall a. Located a -> a
thing (Module -> [Located Prop]
mParamConstraints Module
m)
                     , pFuns :: [(Name, Prop)]
pFuns = [(Name, Prop)]
oks
                     }
     in Params -> Either [Name] Params
forall a b. b -> Either a b
Right Params
ps
  | Bool
otherwise = [Name] -> Either [Name] Params
forall a b. a -> Either a b
Left [Name]
errs
  where
  ([Name]
errs,[(Name, Prop)]
oks) = [Either Name (Name, Prop)] -> ([Name], [(Name, Prop)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers (((Name, ModVParam) -> Either Name (Name, Prop))
-> [(Name, ModVParam)] -> [Either Name (Name, Prop)]
forall a b. (a -> b) -> [a] -> [b]
map (Name, ModVParam) -> Either Name (Name, Prop)
checkFunP (Map Name ModVParam -> [(Name, ModVParam)]
forall k a. Map k a -> [(k, a)]
Map.toList (Module -> Map Name ModVParam
mParamFuns Module
m)))

  checkFunP :: (Name, ModVParam) -> Either Name (Name, Prop)
checkFunP (Name
x,ModVParam
s) = case Schema -> Maybe Prop
isMono (ModVParam -> Schema
mvpType ModVParam
s) of
                      Just Prop
t  -> (Name, Prop) -> Either Name (Name, Prop)
forall a b. b -> Either a b
Right (Name -> Name
asParamName Name
x, Prop
t)
                      Maybe Prop
Nothing -> Name -> Either Name (Name, Prop)
forall a b. a -> Either a b
Left Name
x

  rnTP :: ModTParam -> TParam
rnTP ModTParam
tp = ModTParam -> TParam
mtpParam ModTParam
tp { mtpName :: Name
mtpName = Name -> Name
asParamName (ModTParam -> Name
mtpName ModTParam
tp) }

--------------------------------------------------------------------------------

class AddParams a where
  addParams :: Params -> a -> a

instance AddParams a => AddParams [a] where
  addParams :: Params -> [a] -> [a]
addParams Params
ps = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (Params -> a -> a
forall a. AddParams a => Params -> a -> a
addParams Params
ps)

instance AddParams Schema where
  addParams :: Params -> Schema -> Schema
addParams Params
ps Schema
s = Schema
s { sVars :: [TParam]
sVars  = Params -> [TParam]
pTypes Params
ps [TParam] -> [TParam] -> [TParam]
forall a. [a] -> [a] -> [a]
++ Schema -> [TParam]
sVars Schema
s
                     , sProps :: [Prop]
sProps = Params -> [Prop]
pTypeConstraints Params
ps [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ Schema -> [Prop]
sProps Schema
s
                     , sType :: Prop
sType  = Params -> Prop -> Prop
forall a. AddParams a => Params -> a -> a
addParams Params
ps (Schema -> Prop
sType Schema
s)
                     }

instance AddParams Type where
  addParams :: Params -> Prop -> Prop
addParams Params
ps Prop
t
    | [(Name, Prop)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Params -> [(Name, Prop)]
pFuns Params
ps) = Prop
t
    | Bool
otherwise       = Prop -> Prop -> Prop
tFun (Params -> Prop
paramRecTy Params
ps) Prop
t


instance AddParams Expr where
  addParams :: Params -> Expr -> Expr
addParams Params
ps Expr
e = (TParam -> Expr -> Expr) -> Expr -> [TParam] -> Expr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Expr -> Expr
ETAbs Expr
withProps (Params -> [TParam]
pTypes Params
ps [TParam] -> [TParam] -> [TParam]
forall a. [a] -> [a] -> [a]
++ [TParam]
as)
    where ([TParam]
as,Expr
rest1) = (Expr -> Maybe (TParam, Expr)) -> Expr -> ([TParam], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe (TParam, Expr)
splitTAbs Expr
e
          ([Prop]
bs,Expr
rest2) = (Expr -> Maybe (Prop, Expr)) -> Expr -> ([Prop], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe (Prop, Expr)
splitProofAbs Expr
rest1
          withProps :: Expr
withProps = (Prop -> Expr -> Expr) -> Expr -> [Prop] -> Expr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Expr -> Expr
EProofAbs Expr
withArgs (Params -> [Prop]
pTypeConstraints Params
ps [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop]
bs)
          withArgs :: Expr
withArgs
            | [(Name, Prop)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Params -> [(Name, Prop)]
pFuns Params
ps) = Expr
rest2
            | Bool
otherwise       = Name -> Prop -> Expr -> Expr
EAbs Name
paramModRecParam (Params -> Prop
paramRecTy Params
ps) Expr
rest2



instance AddParams DeclGroup where
  addParams :: Params -> DeclGroup -> DeclGroup
addParams Params
ps DeclGroup
dg =
    case DeclGroup
dg of
      Recursive [Decl]
ds -> [Decl] -> DeclGroup
Recursive (Params -> [Decl] -> [Decl]
forall a. AddParams a => Params -> a -> a
addParams Params
ps [Decl]
ds)
      NonRecursive Decl
d -> Decl -> DeclGroup
NonRecursive (Params -> Decl -> Decl
forall a. AddParams a => Params -> a -> a
addParams Params
ps Decl
d)

instance AddParams Decl where
  addParams :: Params -> Decl -> Decl
addParams Params
ps Decl
d =
    case Decl -> DeclDef
dDefinition Decl
d of
      DeclDef
DPrim   -> Decl
d
      DExpr Expr
e -> Decl
d { dSignature :: Schema
dSignature = Params -> Schema -> Schema
forall a. AddParams a => Params -> a -> a
addParams Params
ps (Decl -> Schema
dSignature Decl
d)
                   , dDefinition :: DeclDef
dDefinition = Expr -> DeclDef
DExpr (Params -> Expr -> Expr
forall a. AddParams a => Params -> a -> a
addParams Params
ps Expr
e)
                   , dName :: Name
dName = Name -> Name
toParamInstName (Decl -> Name
dName Decl
d)
                   }

instance AddParams TySyn where
  addParams :: Params -> TySyn -> TySyn
addParams Params
ps TySyn
ts = TySyn
ts { tsParams :: [TParam]
tsParams = Params -> [TParam]
pTypes Params
ps [TParam] -> [TParam] -> [TParam]
forall a. [a] -> [a] -> [a]
++ TySyn -> [TParam]
tsParams TySyn
ts
                       , tsConstraints :: [Prop]
tsConstraints = Params -> [Prop]
pTypeConstraints Params
ps [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ TySyn -> [Prop]
tsConstraints TySyn
ts
                          --  do we need these here ^ ?
                       , tsName :: Name
tsName = Name -> Name
toParamInstName (TySyn -> Name
tsName TySyn
ts)
                       }

instance AddParams Newtype where
  addParams :: Params -> Newtype -> Newtype
addParams Params
ps Newtype
nt = Newtype
nt { ntParams :: [TParam]
ntParams = Params -> [TParam]
pTypes Params
ps [TParam] -> [TParam] -> [TParam]
forall a. [a] -> [a] -> [a]
++ Newtype -> [TParam]
ntParams Newtype
nt
                       , ntConstraints :: [Prop]
ntConstraints = Params -> [Prop]
pTypeConstraints Params
ps [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ Newtype -> [Prop]
ntConstraints Newtype
nt
                       , ntName :: Name
ntName = Name -> Name
toParamInstName (Newtype -> Name
ntName Newtype
nt)
                       }



--------------------------------------------------------------------------------





-- | Adjust uses of names to account for the new parameters.
-- Assumes unique names---no capture or shadowing.
class Inst a where
  inst :: Inp -> a -> a

-- | Set of top-level names which need to be instantiate, and module parameters.
type Inp = (Set Name, Params)


paramRecTy :: Params -> Type
paramRecTy :: Params -> Prop
paramRecTy Params
ps = RecordMap Ident Prop -> Prop
tRec ([(Ident, Prop)] -> RecordMap Ident Prop
forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields [ (Name -> Ident
nameIdent Name
x, Prop
t) | (Name
x,Prop
t) <- Params -> [(Name, Prop)]
pFuns Params
ps ])


nameInst :: Inp -> Name -> [Type] -> Int -> Expr
nameInst :: (Set Name, Params) -> Name -> [Prop] -> Int -> Expr
nameInst (Set Name
_,Params
ps) Name
x [Prop]
ts Int
prfs
  | [(Name, Prop)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Params -> [(Name, Prop)]
pFuns Params
ps) = Expr
withProofs
  | Bool
otherwise       = Expr -> Expr -> Expr
EApp Expr
withProofs (Name -> Expr
EVar Name
paramModRecParam)
  where
  withProofs :: Expr
withProofs = (Expr -> Expr) -> Expr -> [Expr]
forall a. (a -> a) -> a -> [a]
iterate Expr -> Expr
EProofApp Expr
withTys [Expr] -> Int -> Expr
forall a. [a] -> Int -> a
!!
                                        ([Prop] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Params -> [Prop]
pTypeConstraints Params
ps) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
prfs)

  withTys :: Expr
withTys    = (Expr -> Prop -> Expr) -> Expr -> [Prop] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Prop -> Expr
ETApp (Name -> Expr
EVar (Name -> Name
toParamInstName Name
x))
                           ((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
tpVar) (Params -> [TParam]
pTypes Params
ps) [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop]
ts)


-- | Extra parameters to dd when instantiating a type
instTyParams :: Inp -> [Type]
instTyParams :: (Set Name, Params) -> [Prop]
instTyParams (Set Name
_,Params
ps) = (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
tpVar) (Params -> [TParam]
pTypes Params
ps)


needsInst :: Inp -> Name -> Bool
needsInst :: (Set Name, Params) -> Name -> Bool
needsInst (Set Name
xs,Params
_) Name
x = Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Name
x Set Name
xs

isVParam :: Inp -> Name -> Bool
isVParam :: (Set Name, Params) -> Name -> Bool
isVParam (Set Name
_,Params
ps) Name
x = Name
x Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Name, Prop) -> Name) -> [(Name, Prop)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Prop) -> Name
forall a b. (a, b) -> a
fst (Params -> [(Name, Prop)]
pFuns Params
ps)

isTParam :: Inp -> TVar -> Maybe TParam
isTParam :: (Set Name, Params) -> TVar -> Maybe TParam
isTParam (Set Name
_,Params
ps) TVar
x =
  case TVar
x of
    TVBound TParam
tp -> (TParam -> Bool) -> [TParam] -> Maybe TParam
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find TParam -> Bool
thisName (Params -> [TParam]
pTypes Params
ps)
      where thisName :: TParam -> Bool
thisName TParam
y = TParam -> Maybe Name
tpName TParam
tp Maybe Name -> Maybe Name -> Bool
forall a. Eq a => a -> a -> Bool
== TParam -> Maybe Name
tpName TParam
y
    TVar
_ -> Maybe TParam
forall a. Maybe a
Nothing


instance Inst a => Inst [a] where
  inst :: (Set Name, Params) -> [a] -> [a]
inst (Set Name, Params)
ps = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map ((Set Name, Params) -> a -> a
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps)

instance Inst Expr where
  inst :: (Set Name, Params) -> Expr -> Expr
inst (Set Name, Params)
ps Expr
expr =
    case Expr
expr of
     EVar Name
x
      | (Set Name, Params) -> Name -> Bool
needsInst (Set Name, Params)
ps Name
x -> (Set Name, Params) -> Name -> [Prop] -> Int -> Expr
nameInst (Set Name, Params)
ps Name
x [] Int
0
      | (Set Name, Params) -> Name -> Bool
isVParam (Set Name, Params)
ps Name
x ->
        let sh :: [Ident]
sh = ((Name, Prop) -> Ident) -> [(Name, Prop)] -> [Ident]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Ident
nameIdent (Name -> Ident) -> ((Name, Prop) -> Name) -> (Name, Prop) -> Ident
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Prop) -> Name
forall a b. (a, b) -> a
fst) (Params -> [(Name, Prop)]
pFuns ((Set Name, Params) -> Params
forall a b. (a, b) -> b
snd (Set Name, Params)
ps))
        in Expr -> Selector -> Expr
ESel (Name -> Expr
EVar Name
paramModRecParam) (Ident -> Maybe [Ident] -> Selector
RecordSel (Name -> Ident
nameIdent Name
x) ([Ident] -> Maybe [Ident]
forall a. a -> Maybe a
Just [Ident]
sh))
      | Bool
otherwise -> Name -> Expr
EVar Name
x

     EList [Expr]
es Prop
t -> [Expr] -> Prop -> Expr
EList ((Set Name, Params) -> [Expr] -> [Expr]
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps [Expr]
es) ((Set Name, Params) -> Prop -> Prop
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Prop
t)
     ETuple [Expr]
es -> [Expr] -> Expr
ETuple ((Set Name, Params) -> [Expr] -> [Expr]
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps [Expr]
es)
     ERec RecordMap Ident Expr
fs   -> RecordMap Ident Expr -> Expr
ERec ((Expr -> Expr) -> RecordMap Ident Expr -> RecordMap Ident Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Set Name, Params) -> Expr -> Expr
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps) RecordMap Ident Expr
fs)
     ESel Expr
e Selector
s  -> Expr -> Selector -> Expr
ESel ((Set Name, Params) -> Expr -> Expr
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Expr
e) Selector
s
     ESet Prop
ty Expr
e Selector
s Expr
v -> Prop -> Expr -> Selector -> Expr -> Expr
ESet ((Set Name, Params) -> Prop -> Prop
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Prop
ty) ((Set Name, Params) -> Expr -> Expr
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Expr
e) Selector
s ((Set Name, Params) -> Expr -> Expr
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Expr
v)

     EIf Expr
e1 Expr
e2 Expr
e3 -> Expr -> Expr -> Expr -> Expr
EIf ((Set Name, Params) -> Expr -> Expr
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Expr
e1) ((Set Name, Params) -> Expr -> Expr
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Expr
e2) ((Set Name, Params) -> Expr -> Expr
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Expr
e3)
     EComp Prop
t1 Prop
t2 Expr
e [[Match]]
ms -> Prop -> Prop -> Expr -> [[Match]] -> Expr
EComp ((Set Name, Params) -> Prop -> Prop
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Prop
t1) ((Set Name, Params) -> Prop -> Prop
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Prop
t2)
                               ((Set Name, Params) -> Expr -> Expr
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Expr
e) ((Set Name, Params) -> [[Match]] -> [[Match]]
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps [[Match]]
ms)

     ETAbs TParam
x Expr
e -> TParam -> Expr -> Expr
ETAbs TParam
x ((Set Name, Params) -> Expr -> Expr
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Expr
e)
     ETApp Expr
e1 Prop
t ->
      case Expr -> (Expr, [Prop], Int)
splitExprInst Expr
expr of
         (EVar Name
x, [Prop]
ts, Int
prfs) | (Set Name, Params) -> Name -> Bool
needsInst (Set Name, Params)
ps Name
x -> (Set Name, Params) -> Name -> [Prop] -> Int -> Expr
nameInst (Set Name, Params)
ps Name
x [Prop]
ts Int
prfs
         (Expr, [Prop], Int)
_ -> Expr -> Prop -> Expr
ETApp ((Set Name, Params) -> Expr -> Expr
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Expr
e1) Prop
t

     EApp Expr
e1 Expr
e2 -> Expr -> Expr -> Expr
EApp ((Set Name, Params) -> Expr -> Expr
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Expr
e1) ((Set Name, Params) -> Expr -> Expr
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Expr
e2)
     EAbs Name
x Prop
t Expr
e -> Name -> Prop -> Expr -> Expr
EAbs Name
x ((Set Name, Params) -> Prop -> Prop
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Prop
t) ((Set Name, Params) -> Expr -> Expr
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Expr
e)

     EProofAbs Prop
p Expr
e -> Prop -> Expr -> Expr
EProofAbs ((Set Name, Params) -> Prop -> Prop
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Prop
p) ((Set Name, Params) -> Expr -> Expr
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Expr
e)
     EProofApp Expr
e1 ->
       case Expr -> (Expr, [Prop], Int)
splitExprInst Expr
expr of
         (EVar Name
x, [Prop]
ts, Int
prfs) | (Set Name, Params) -> Name -> Bool
needsInst (Set Name, Params)
ps Name
x -> (Set Name, Params) -> Name -> [Prop] -> Int -> Expr
nameInst (Set Name, Params)
ps Name
x [Prop]
ts Int
prfs
         (Expr, [Prop], Int)
_ -> Expr -> Expr
EProofApp ((Set Name, Params) -> Expr -> Expr
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Expr
e1)

     EWhere Expr
e [DeclGroup]
dgs  -> Expr -> [DeclGroup] -> Expr
EWhere ((Set Name, Params) -> Expr -> Expr
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Expr
e) ((Set Name, Params) -> [DeclGroup] -> [DeclGroup]
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps [DeclGroup]
dgs)


instance Inst Match where
  inst :: (Set Name, Params) -> Match -> Match
inst (Set Name, Params)
ps Match
m =
    case Match
m of
      From Name
x Prop
t1 Prop
t2 Expr
e -> Name -> Prop -> Prop -> Expr -> Match
From Name
x ((Set Name, Params) -> Prop -> Prop
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Prop
t1) ((Set Name, Params) -> Prop -> Prop
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Prop
t2) ((Set Name, Params) -> Expr -> Expr
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Expr
e)
      Let Decl
d          -> Decl -> Match
Let ((Set Name, Params) -> Decl -> Decl
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Decl
d)

instance Inst DeclGroup where
  inst :: (Set Name, Params) -> DeclGroup -> DeclGroup
inst (Set Name, Params)
ps DeclGroup
dg =
    case DeclGroup
dg of
      Recursive [Decl]
ds -> [Decl] -> DeclGroup
Recursive ((Set Name, Params) -> [Decl] -> [Decl]
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps [Decl]
ds)
      NonRecursive Decl
d -> Decl -> DeclGroup
NonRecursive ((Set Name, Params) -> Decl -> Decl
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Decl
d)

instance Inst Decl where
  inst :: (Set Name, Params) -> Decl -> Decl
inst (Set Name, Params)
ps Decl
d = Decl
d { dDefinition :: DeclDef
dDefinition = (Set Name, Params) -> DeclDef -> DeclDef
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps (Decl -> DeclDef
dDefinition Decl
d) }

instance Inst DeclDef where
  inst :: (Set Name, Params) -> DeclDef -> DeclDef
inst (Set Name, Params)
ps DeclDef
d =
    case DeclDef
d of
      DeclDef
DPrim -> DeclDef
DPrim
      DExpr Expr
e -> Expr -> DeclDef
DExpr ((Set Name, Params) -> Expr -> Expr
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Expr
e)

instance Inst Type where
  inst :: (Set Name, Params) -> Prop -> Prop
inst (Set Name, Params)
ps Prop
ty =
    case Prop
ty of
      TUser Name
x [Prop]
ts Prop
t
        | (Set Name, Params) -> Name -> Bool
needsInst (Set Name, Params)
ps Name
x -> Name -> [Prop] -> Prop -> Prop
TUser Name
x ((Set Name, Params) -> [Prop]
instTyParams (Set Name, Params)
ps [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop]
ts1) Prop
t1
        | Bool
otherwise      -> Name -> [Prop] -> Prop -> Prop
TUser Name
x [Prop]
ts1 Prop
t1
        where ts1 :: [Prop]
ts1 = (Set Name, Params) -> [Prop] -> [Prop]
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps [Prop]
ts
              t1 :: Prop
t1  = (Set Name, Params) -> Prop -> Prop
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Prop
t

      TCon TCon
tc [Prop]
ts ->
        case TCon
tc of
          TC (TCNewtype (UserTC Name
x Kind
k))
            | (Set Name, Params) -> Name -> Bool
needsInst (Set Name, Params)
ps Name
x -> TCon -> [Prop] -> Prop
TCon (TC -> TCon
TC (UserTC -> TC
TCNewtype (Name -> Kind -> UserTC
UserTC Name
x (Kind -> Kind
k1 Kind
k))))
                                     ([Prop]
newTs [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [Prop]
ts1)
          TCon
_ -> TCon -> [Prop] -> Prop
TCon TCon
tc [Prop]
ts1
        where
        ts1 :: [Prop]
ts1 = (Set Name, Params) -> [Prop] -> [Prop]
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps [Prop]
ts
        newTs :: [Prop]
newTs = (Set Name, Params) -> [Prop]
instTyParams (Set Name, Params)
ps
        k1 :: Kind -> Kind
k1 Kind
k = (Kind -> Kind -> Kind) -> Kind -> [Kind] -> Kind
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Kind -> Kind -> Kind
(:->) Kind
k ((Prop -> Kind) -> [Prop] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map Prop -> Kind
forall t. HasKind t => t -> Kind
kindOf [Prop]
newTs)

      TVar TVar
x | Just TParam
x' <- (Set Name, Params) -> TVar -> Maybe TParam
isTParam (Set Name, Params)
ps TVar
x -> TVar -> Prop
TVar (TParam -> TVar
TVBound TParam
x')
             | Bool
otherwise  -> Prop
ty

      TRec RecordMap Ident Prop
xs -> RecordMap Ident Prop -> Prop
TRec ((Prop -> Prop) -> RecordMap Ident Prop -> RecordMap Ident Prop
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Set Name, Params) -> Prop -> Prop
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps) RecordMap Ident Prop
xs)

instance Inst TySyn where
  inst :: (Set Name, Params) -> TySyn -> TySyn
inst (Set Name, Params)
ps TySyn
ts = TySyn
ts { tsConstraints :: [Prop]
tsConstraints = (Set Name, Params) -> [Prop] -> [Prop]
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps (TySyn -> [Prop]
tsConstraints TySyn
ts)
                  , tsDef :: Prop
tsDef = (Set Name, Params) -> Prop -> Prop
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps (TySyn -> Prop
tsDef TySyn
ts)
                  }

instance Inst Newtype where
  inst :: (Set Name, Params) -> Newtype -> Newtype
inst (Set Name, Params)
ps Newtype
nt = Newtype
nt { ntConstraints :: [Prop]
ntConstraints = (Set Name, Params) -> [Prop] -> [Prop]
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps (Newtype -> [Prop]
ntConstraints Newtype
nt)
                  , ntFields :: [(Ident, Prop)]
ntFields = [ (Ident
f, (Set Name, Params) -> Prop -> Prop
forall a. Inst a => (Set Name, Params) -> a -> a
inst (Set Name, Params)
ps Prop
t) | (Ident
f,Prop
t) <- Newtype -> [(Ident, Prop)]
ntFields Newtype
nt ]
                  }