{-# LANGUAGE OverloadedStrings #-}
module Funcons.TypeSubstitution where
import Funcons.Types
import Funcons.Patterns
import qualified Data.Map as M
import qualified Data.Set as S
type TypeEnv = M.Map MetaVar TyAssoc
data TyAssoc = ElemOf FTerm | SubTyOf FTerm
limitedSubsTypeVar :: HasTypeVar a => S.Set MetaVar -> TypeEnv -> a -> a
limitedSubsTypeVar :: forall a. HasTypeVar a => Set MetaVar -> TypeEnv -> a -> a
limitedSubsTypeVar Set MetaVar
pvars TypeEnv
env = forall a. HasTypeVar a => TypeEnv -> a -> a
subsTypeVar (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {k} {a}. Ord k => k -> Map k a -> Map k a
aux TypeEnv
env Set MetaVar
pvars)
where aux :: k -> Map k a -> Map k a
aux k
pvar = forall {k} {a}. Ord k => k -> Map k a -> Map k a
M.delete k
pvar
limitedSubsTypeVarWildcard :: HasTypeVar a => S.Set MetaVar -> Maybe FTerm -> TypeEnv -> a -> a
limitedSubsTypeVarWildcard :: forall a.
HasTypeVar a =>
Set MetaVar -> Maybe FTerm -> TypeEnv -> a -> a
limitedSubsTypeVarWildcard Set MetaVar
pvars Maybe FTerm
mt TypeEnv
env = forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {k} {a}. Ord k => k -> Map k a -> Map k a
aux TypeEnv
env Set MetaVar
pvars)
where aux :: k -> Map k a -> Map k a
aux k
pvar = forall {k} {a}. Ord k => k -> Map k a -> Map k a
M.delete k
pvar
class HasTypeVar a where
subsTypeVar :: TypeEnv -> a -> a
subsTypeVar = forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard forall a. Maybe a
Nothing
subsTypeVarWildcard :: (Maybe FTerm) -> TypeEnv -> a -> a
instance HasTypeVar FTerm where
subsTypeVarWildcard :: Maybe FTerm -> TypeEnv -> FTerm -> FTerm
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
t = case FTerm
t of
TVar MetaVar
var -> case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup MetaVar
var TypeEnv
env of
Just (SubTyOf FTerm
ty) -> FTerm
ty
Just (ElemOf (TSortSeq (TName Name
"types") SeqSortOp
op)) -> FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
op
Just (ElemOf (TSortSeq (TName Name
"value-types") SeqSortOp
op)) -> FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
op
Just (ElemOf (TName Name
"types")) -> Name -> FTerm
TName Name
"values"
Just (ElemOf FTerm
vt) -> MetaVar -> FTerm
TVar MetaVar
var
Maybe TyAssoc
Nothing -> MetaVar -> FTerm
TVar MetaVar
var
TName Name
nm -> Name -> FTerm
TName Name
nm
TApp Name
nm [FTerm]
ts-> Name -> [FTerm] -> FTerm
TApp Name
nm (forall a b. (a -> b) -> [a] -> [b]
map (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env) [FTerm]
ts)
TSeq [FTerm]
ts -> [FTerm] -> FTerm
TSeq (forall a b. (a -> b) -> [a] -> [b]
map (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env) [FTerm]
ts)
TSet [FTerm]
ts -> [FTerm] -> FTerm
TSet (forall a b. (a -> b) -> [a] -> [b]
map (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env) [FTerm]
ts)
TMap [FTerm]
ts -> [FTerm] -> FTerm
TMap (forall a b. (a -> b) -> [a] -> [b]
map (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env) [FTerm]
ts)
TBinding FTerm
x FTerm
y -> FTerm -> FTerm -> FTerm
TBinding (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
x) (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
y)
TFuncon Funcons
f -> Funcons -> FTerm
TFuncon Funcons
f
TSortSeq FTerm
t SeqSortOp
op -> FTerm -> SeqSortOp -> FTerm
TSortSeq (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
t) SeqSortOp
op
TSortPower FTerm
t1 FTerm
t2 -> FTerm -> FTerm -> FTerm
TSortPower (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
t1) (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
t2)
TSortUnion FTerm
t1 FTerm
t2 -> FTerm -> FTerm -> FTerm
TSortUnion (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
t1) (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
t2)
TSortInter FTerm
t1 FTerm
t2 -> FTerm -> FTerm -> FTerm
TSortInter (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
t1) (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
t2)
TSortComplement FTerm
t -> FTerm -> FTerm
TSortComplement (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
t)
TSortComputes FTerm
t -> FTerm -> FTerm
TSortComputes (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
t)
TSortComputesFrom FTerm
f FTerm
t -> FTerm -> FTerm -> FTerm
TSortComputesFrom (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
f) (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
t)
FTerm
TAny -> case Maybe FTerm
mt of Maybe FTerm
Nothing -> FTerm
TAny
Just FTerm
t -> FTerm
t
instance HasTypeVar VPattern where
subsTypeVarWildcard :: Maybe FTerm -> TypeEnv -> VPattern -> VPattern
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env VPattern
pat = case VPattern
pat of
VPAnnotated VPattern
p FTerm
t -> VPattern -> FTerm -> VPattern
VPAnnotated (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env VPattern
p) (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
t)
PADT Name
n [VPattern]
pats -> Name -> [VPattern] -> VPattern
PADT Name
n (forall a b. (a -> b) -> [a] -> [b]
map (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env) [VPattern]
pats)
VPMetaVar MetaVar
var -> MetaVar -> VPattern
VPMetaVar MetaVar
var
VPSeqVar MetaVar
var SeqSortOp
op -> MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
var SeqSortOp
op
VPLit Values
v -> Values -> VPattern
VPLit Values
v
VPattern
VPWildCard -> VPattern
VPWildCard
VPType TPattern
pat -> TPattern -> VPattern
VPType TPattern
pat
VPattern
VPEmptySet -> VPattern
VPEmptySet
instance HasTypeVar FPattern where
subsTypeVarWildcard :: Maybe FTerm -> TypeEnv -> FPattern -> FPattern
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FPattern
pat = case FPattern
pat of
PAnnotated FPattern
p FTerm
t -> FPattern -> FTerm -> FPattern
PAnnotated (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FPattern
p) (forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
t)
PValue VPattern
p -> VPattern -> FPattern
PValue forall a b. (a -> b) -> a -> b
$ forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env VPattern
p
PMetaVar MetaVar
var -> MetaVar -> FPattern
PMetaVar MetaVar
var
PSeqVar MetaVar
var SeqSortOp
op -> MetaVar -> SeqSortOp -> FPattern
PSeqVar MetaVar
var SeqSortOp
op
FPattern
PWildCard -> FPattern
PWildCard