{-# LANGUAGE OverloadedStrings #-}

module Funcons.TypeSubstitution where

import Funcons.Types
import Funcons.Patterns

import qualified Data.Map as M
import qualified Data.Set as S

-- | Associates types (Terms) with meta-variables 
type TypeEnv = M.Map MetaVar TyAssoc
data TyAssoc = ElemOf FTerm | SubTyOf FTerm

-- | Version of `subsTypeVar` that does not replace the meta-variables
-- in the given set
limitedSubsTypeVar :: HasTypeVar a => S.Set MetaVar -> TypeEnv -> a -> a
limitedSubsTypeVar :: Set MetaVar -> TypeEnv -> a -> a
limitedSubsTypeVar Set MetaVar
pvars TypeEnv
env = TypeEnv -> a -> a
forall a. HasTypeVar a => TypeEnv -> a -> a
subsTypeVar ((MetaVar -> TypeEnv -> TypeEnv)
-> TypeEnv -> Set MetaVar -> TypeEnv
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr MetaVar -> TypeEnv -> TypeEnv
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 = k -> Map k a -> Map k a
forall k a. Ord k => k -> Map k a -> Map k a
M.delete k
pvar

-- | Version of `subsTypeVarWildcard` that does not replace the meta-variables
-- in the given set
limitedSubsTypeVarWildcard :: HasTypeVar a => S.Set MetaVar -> Maybe FTerm -> TypeEnv -> a -> a
limitedSubsTypeVarWildcard :: Set MetaVar -> Maybe FTerm -> TypeEnv -> a -> a
limitedSubsTypeVarWildcard Set MetaVar
pvars Maybe FTerm
mt TypeEnv
env = Maybe FTerm -> TypeEnv -> a -> a
forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt ((MetaVar -> TypeEnv -> TypeEnv)
-> TypeEnv -> Set MetaVar -> TypeEnv
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr MetaVar -> TypeEnv -> TypeEnv
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 = k -> Map k a -> Map k a
forall k a. Ord k => k -> Map k a -> Map k a
M.delete k
pvar


-- | Used for replacing meta-variables `T` in pattern annotations `P:T` with
-- the type to which `T` is bound in some type-environment (if any)
class HasTypeVar a where
  subsTypeVar :: TypeEnv -> a -> a
  subsTypeVar = Maybe FTerm -> TypeEnv -> a -> a
forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
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 MetaVar -> TypeEnv -> Maybe TyAssoc
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 ((FTerm -> FTerm) -> [FTerm] -> [FTerm]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe FTerm -> TypeEnv -> FTerm -> FTerm
forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env) [FTerm]
ts)
    TSeq [FTerm]
ts -> [FTerm] -> FTerm
TSeq ((FTerm -> FTerm) -> [FTerm] -> [FTerm]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe FTerm -> TypeEnv -> FTerm -> FTerm
forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env) [FTerm]
ts)
--    TList ts  -> TList (map (subsTypeVarWildcard mt env) ts)
    TSet  [FTerm]
ts  -> [FTerm] -> FTerm
TSet ((FTerm -> FTerm) -> [FTerm] -> [FTerm]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe FTerm -> TypeEnv -> FTerm -> FTerm
forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env) [FTerm]
ts)
    TMap [FTerm]
ts   -> [FTerm] -> FTerm
TMap ((FTerm -> FTerm) -> [FTerm] -> [FTerm]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe FTerm -> TypeEnv -> FTerm -> FTerm
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 (Maybe FTerm -> TypeEnv -> FTerm -> FTerm
forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
x) (Maybe FTerm -> TypeEnv -> FTerm -> FTerm
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 (Maybe FTerm -> TypeEnv -> FTerm -> FTerm
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 (Maybe FTerm -> TypeEnv -> FTerm -> FTerm
forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
t1) (Maybe FTerm -> TypeEnv -> FTerm -> FTerm
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 (Maybe FTerm -> TypeEnv -> FTerm -> FTerm
forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
t1) (Maybe FTerm -> TypeEnv -> FTerm -> FTerm
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 (Maybe FTerm -> TypeEnv -> FTerm -> FTerm
forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
t1) (Maybe FTerm -> TypeEnv -> FTerm -> FTerm
forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
t2)
    TSortComplement FTerm
t -> FTerm -> FTerm
TSortComplement (Maybe FTerm -> TypeEnv -> FTerm -> FTerm
forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
t)
    TSortComputes FTerm
t -> FTerm -> FTerm
TSortComputes (Maybe FTerm -> TypeEnv -> FTerm -> FTerm
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 (Maybe FTerm -> TypeEnv -> FTerm -> FTerm
forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
f) (Maybe FTerm -> TypeEnv -> FTerm -> FTerm
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 (Maybe FTerm -> TypeEnv -> VPattern -> VPattern
forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env VPattern
p) (Maybe FTerm -> TypeEnv -> FTerm -> FTerm
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 ((VPattern -> VPattern) -> [VPattern] -> [VPattern]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe FTerm -> TypeEnv -> VPattern -> VPattern
forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env) [VPattern]
pats)
--    PList pats        -> PList (map (subsTypeVarWildcard mt env) 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 

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 (Maybe FTerm -> TypeEnv -> FPattern -> FPattern
forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FPattern
p) (Maybe FTerm -> TypeEnv -> FTerm -> FTerm
forall a. HasTypeVar a => Maybe FTerm -> TypeEnv -> a -> a
subsTypeVarWildcard Maybe FTerm
mt TypeEnv
env FTerm
t)
    PValue VPattern
p        -> VPattern -> FPattern
PValue (VPattern -> FPattern) -> VPattern -> FPattern
forall a b. (a -> b) -> a -> b
$ Maybe FTerm -> TypeEnv -> VPattern -> VPattern
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