content: {-# LANGUAGE FlexibleInstances #-}
  module Language.Fixpoint.Types.Templates (
  
    anything, Templates, makeTemplates,
  
    isEmptyTemplates, isAnyTemplates,
  
    matchesTemplates, filterUnMatched
  
    )where
  
  import Language.Fixpoint.Types.Refinements
  import Language.Fixpoint.Types.Names
  import Language.Fixpoint.Types.PrettyPrint
  import Text.PrettyPrint.HughesPJ.Compat
  
  data Templates
    = TAll
    | TExprs [Template]
    deriving Show
  
  
  type Template = ([Symbol], Expr)
  
  
  class HasTemplates a where
    filterUnMatched :: Templates -> a -> a
  
  
  instance HasTemplates Expr where
    filterUnMatched temps e = pAnd $ filter (not . matchesTemplates temps) $ conjuncts e
  
  instance HasTemplates Reft where
    filterUnMatched temps (Reft (x,e)) = Reft (x, filterUnMatched temps e)
  
  matchesTemplates :: Templates -> Expr -> Bool
  matchesTemplates TAll _ = True
  matchesTemplates (TExprs ts) e = any (`matchesTemplate` e) ts
  
  matchesTemplate :: Template -> Expr -> Bool
  matchesTemplate (xs, t@(EVar x)) e
    = x `elem` xs || e == t
  matchesTemplate (xs, EApp t1 t2) (EApp e1 e2)
    = matchesTemplate (xs, t1) e1 && matchesTemplate (xs, t2) e2
  matchesTemplate (xs, ENeg t) (ENeg e)
    = matchesTemplate (xs, t) e
  matchesTemplate (xs, EBin b t1 t2) (EBin b' e1 e2)
    = b == b' && matchesTemplate (xs, t1) e1 && matchesTemplate (xs, t2) e2
  matchesTemplate (xs, ELet x t1 t2) (ELet x' e1 e2)
    = x == x' && matchesTemplate (xs, t1) e1 && matchesTemplate (xs, t2) e2
  matchesTemplate (xs, EIte t1 t2 t3) (EIte e1 e2 e3)
    = matchesTemplate (xs, t1) e1 && matchesTemplate (xs, t2) e2 && matchesTemplate (xs, t3) e3
  matchesTemplate (xs, ECst t s) (ECst e s')
    = s == s' && matchesTemplate (xs, t) e
  matchesTemplate (xs, ELam b t) (ELam b' e)
    = b == b' && matchesTemplate (xs, t) e
  matchesTemplate (xs, ETApp t s) (ETApp e s')
    = s == s' && matchesTemplate (xs, t) e
  matchesTemplate (xs, ETAbs t s) (ETAbs e s')
    = s == s' && matchesTemplate (xs, t) e
  matchesTemplate (xs, PNot t) (PNot e)
    = matchesTemplate (xs, t) e
  matchesTemplate (xs, PAnd ts) (PAnd es)
    = and $ zipWith (\t e -> matchesTemplate (xs, t) e) ts es
  matchesTemplate (xs, POr ts) (POr es)
    = and $ zipWith (\t e -> matchesTemplate (xs, t) e) ts es
  matchesTemplate (xs, PImp t1 t2) (PImp e1 e2)
    = matchesTemplate (xs, t1) e1 && matchesTemplate (xs, t2) e2
  matchesTemplate (xs, PIff t1 t2) (PIff e1 e2)
    = matchesTemplate (xs, t1) e1 && matchesTemplate (xs, t2) e2
  matchesTemplate (xs, PAtom b t1 t2) (PAtom b' e1 e2)
    = b == b' && matchesTemplate (xs, t1) e1 && matchesTemplate (xs, t2) e2
  matchesTemplate (xs, PAll s t) (PAll s' e)
    = s == s' && matchesTemplate (xs, t) e
  matchesTemplate (xs, PExist s t) (PExist s' e)
    = s == s' && matchesTemplate (xs, t) e
  matchesTemplate (xs, PGrad s1 s2 s3 t) (PGrad s1' s2' s3' e)
    = s1 == s1' && s2 == s2' && s3 == s3' && matchesTemplate (xs, t) e
  matchesTemplate (xs, ECoerc s1 s2 t) (ECoerc s1' s2' e)
    = s1 == s1' && s2 == s2' && matchesTemplate (xs, t) e
  matchesTemplate (_, t) e
    = t == e
  
  
  
  makeTemplates :: [([Symbol], Expr)] -> Templates
  makeTemplates = TExprs
  
  
  isEmptyTemplates, isAnyTemplates :: Templates -> Bool
  isEmptyTemplates (TExprs []) = True
  isEmptyTemplates _           = False
  
  isAnyTemplates TAll = True
  isAnyTemplates _    = False
  
  anything :: Templates
  anything = TAll
  
  instance Semigroup Templates where
    TAll <> _ = TAll
    _ <> TAll = TAll
    TExprs i1 <> TExprs i2 = TExprs (i1 ++ i2)
  
  instance Monoid Templates where
    mempty = TExprs []
  
  instance PPrint Templates where
    pprintTidy _ = text . show
  