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 Int -> Templates -> ShowS
[Templates] -> ShowS
Templates -> String
(Int -> Templates -> ShowS)
-> (Templates -> String)
-> ([Templates] -> ShowS)
-> Show Templates
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Templates] -> ShowS
$cshowList :: [Templates] -> ShowS
show :: Templates -> String
$cshow :: Templates -> String
showsPrec :: Int -> Templates -> ShowS
$cshowsPrec :: Int -> Templates -> ShowS
Show


type Template = ([Symbol], Expr)


class HasTemplates a where 
  filterUnMatched :: Templates -> a -> a 


instance HasTemplates Expr where
  filterUnMatched :: Templates -> Expr -> Expr
filterUnMatched Templates
temps Expr
e = ListNE Expr -> Expr
pAnd (ListNE Expr -> Expr) -> ListNE Expr -> Expr
forall a b. (a -> b) -> a -> b
$ (Expr -> Bool) -> ListNE Expr -> ListNE Expr
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Templates -> Expr -> Bool
matchesTemplates Templates
temps) (ListNE Expr -> ListNE Expr) -> ListNE Expr -> ListNE Expr
forall a b. (a -> b) -> a -> b
$ Expr -> ListNE Expr
conjuncts Expr
e 

instance HasTemplates Reft where
  filterUnMatched :: Templates -> Reft -> Reft
filterUnMatched Templates
temps (Reft (Symbol
x,Expr
e)) = (Symbol, Expr) -> Reft
Reft (Symbol
x, Templates -> Expr -> Expr
forall a. HasTemplates a => Templates -> a -> a
filterUnMatched Templates
temps Expr
e)

matchesTemplates :: Templates -> Expr -> Bool 
matchesTemplates :: Templates -> Expr -> Bool
matchesTemplates Templates
TAll Expr
_ = Bool
True 
matchesTemplates (TExprs [Template]
ts) Expr
e = (Template -> Bool) -> [Template] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Template -> Expr -> Bool
`matchesTemplate` Expr
e) [Template]
ts

matchesTemplate :: Template -> Expr -> Bool 
matchesTemplate :: Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, t :: Expr
t@(EVar Symbol
x)) Expr
e
  = Symbol
x Symbol -> [Symbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol]
xs Bool -> Bool -> Bool
|| Expr
e Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
t  
matchesTemplate ([Symbol]
xs, EApp Expr
t1 Expr
t2) (EApp Expr
e1 Expr
e2) 
  = Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t1) Expr
e1 Bool -> Bool -> Bool
&& Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t2) Expr
e2 
matchesTemplate ([Symbol]
xs, ENeg Expr
t) (ENeg Expr
e) 
  = Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t) Expr
e
matchesTemplate ([Symbol]
xs, EBin Bop
b Expr
t1 Expr
t2) (EBin Bop
b' Expr
e1 Expr
e2) 
  = Bop
b Bop -> Bop -> Bool
forall a. Eq a => a -> a -> Bool
== Bop
b' Bool -> Bool -> Bool
&& Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t1) Expr
e1 Bool -> Bool -> Bool
&& Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t2) Expr
e2 
matchesTemplate ([Symbol]
xs, EIte Expr
t1 Expr
t2 Expr
t3) (EIte Expr
e1 Expr
e2 Expr
e3) 
  = Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t1) Expr
e1 Bool -> Bool -> Bool
&& Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t2) Expr
e2 Bool -> Bool -> Bool
&& Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t3) Expr
e3 
matchesTemplate ([Symbol]
xs, ECst Expr
t Sort
s) (ECst Expr
e Sort
s') 
  = Sort
s Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
s' Bool -> Bool -> Bool
&& Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t) Expr
e
matchesTemplate ([Symbol]
xs, ELam (Symbol, Sort)
b Expr
t) (ELam (Symbol, Sort)
b' Expr
e) 
  = (Symbol, Sort)
b (Symbol, Sort) -> (Symbol, Sort) -> Bool
forall a. Eq a => a -> a -> Bool
== (Symbol, Sort)
b' Bool -> Bool -> Bool
&& Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t) Expr
e
matchesTemplate ([Symbol]
xs, ETApp Expr
t Sort
s) (ETApp Expr
e Sort
s') 
  = Sort
s Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
s' Bool -> Bool -> Bool
&& Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t) Expr
e
matchesTemplate ([Symbol]
xs, ETAbs Expr
t Symbol
s) (ETAbs Expr
e Symbol
s') 
  = Symbol
s Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
s' Bool -> Bool -> Bool
&& Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t) Expr
e
matchesTemplate ([Symbol]
xs, PNot Expr
t) (PNot Expr
e) 
  = Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t) Expr
e
matchesTemplate ([Symbol]
xs, PAnd ListNE Expr
ts) (PAnd ListNE Expr
es) 
  = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (Expr -> Expr -> Bool) -> ListNE Expr -> ListNE Expr -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Expr
t Expr
e -> Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t) Expr
e) ListNE Expr
ts ListNE Expr
es 
matchesTemplate ([Symbol]
xs, POr ListNE Expr
ts) (POr ListNE Expr
es) 
  = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (Expr -> Expr -> Bool) -> ListNE Expr -> ListNE Expr -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Expr
t Expr
e -> Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t) Expr
e) ListNE Expr
ts ListNE Expr
es 
matchesTemplate ([Symbol]
xs, PImp Expr
t1 Expr
t2) (PImp Expr
e1 Expr
e2) 
  = Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t1) Expr
e1 Bool -> Bool -> Bool
&& Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t2) Expr
e2 
matchesTemplate ([Symbol]
xs, PIff Expr
t1 Expr
t2) (PIff Expr
e1 Expr
e2) 
  = Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t1) Expr
e1 Bool -> Bool -> Bool
&& Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t2) Expr
e2 
matchesTemplate ([Symbol]
xs, PAtom Brel
b Expr
t1 Expr
t2) (PAtom Brel
b' Expr
e1 Expr
e2) 
  = Brel
b Brel -> Brel -> Bool
forall a. Eq a => a -> a -> Bool
== Brel
b' Bool -> Bool -> Bool
&& Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t1) Expr
e1 Bool -> Bool -> Bool
&& Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t2) Expr
e2 
matchesTemplate ([Symbol]
xs, PAll [(Symbol, Sort)]
s Expr
t) (PAll [(Symbol, Sort)]
s' Expr
e) 
  = [(Symbol, Sort)]
s [(Symbol, Sort)] -> [(Symbol, Sort)] -> Bool
forall a. Eq a => a -> a -> Bool
== [(Symbol, Sort)]
s' Bool -> Bool -> Bool
&& Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t) Expr
e
matchesTemplate ([Symbol]
xs, PExist [(Symbol, Sort)]
s Expr
t) (PExist [(Symbol, Sort)]
s' Expr
e) 
  = [(Symbol, Sort)]
s [(Symbol, Sort)] -> [(Symbol, Sort)] -> Bool
forall a. Eq a => a -> a -> Bool
== [(Symbol, Sort)]
s' Bool -> Bool -> Bool
&& Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t) Expr
e
matchesTemplate ([Symbol]
xs, PGrad KVar
s1 Subst
s2 GradInfo
s3 Expr
t) (PGrad KVar
s1' Subst
s2' GradInfo
s3' Expr
e) 
  = KVar
s1 KVar -> KVar -> Bool
forall a. Eq a => a -> a -> Bool
== KVar
s1' Bool -> Bool -> Bool
&& Subst
s2 Subst -> Subst -> Bool
forall a. Eq a => a -> a -> Bool
== Subst
s2' Bool -> Bool -> Bool
&& GradInfo
s3 GradInfo -> GradInfo -> Bool
forall a. Eq a => a -> a -> Bool
== GradInfo
s3' Bool -> Bool -> Bool
&& Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t) Expr
e
matchesTemplate ([Symbol]
xs, ECoerc Sort
s1 Sort
s2 Expr
t) (ECoerc Sort
s1' Sort
s2' Expr
e) 
  = Sort
s1 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
s1' Bool -> Bool -> Bool
&& Sort
s2 Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
s2' Bool -> Bool -> Bool
&& Template -> Expr -> Bool
matchesTemplate ([Symbol]
xs, Expr
t) Expr
e
matchesTemplate ([Symbol]
_, Expr
t) Expr
e 
  = Expr
t Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e 



makeTemplates :: [([Symbol], Expr)] -> Templates
makeTemplates :: [Template] -> Templates
makeTemplates = [Template] -> Templates
TExprs 


isEmptyTemplates, isAnyTemplates :: Templates -> Bool 
isEmptyTemplates :: Templates -> Bool
isEmptyTemplates (TExprs []) = Bool
True 
isEmptyTemplates Templates
_           = Bool
False 

isAnyTemplates :: Templates -> Bool
isAnyTemplates Templates
TAll = Bool
True 
isAnyTemplates Templates
_    = Bool
False 

anything :: Templates
anything :: Templates
anything = Templates
TAll

instance Semigroup Templates where 
  Templates
TAll <> :: Templates -> Templates -> Templates
<> Templates
_ = Templates
TAll
  Templates
_ <> Templates
TAll = Templates
TAll
  TExprs [Template]
i1 <> TExprs [Template]
i2 = [Template] -> Templates
TExprs ([Template]
i1 [Template] -> [Template] -> [Template]
forall a. [a] -> [a] -> [a]
++ [Template]
i2)

instance Monoid Templates where 
  mempty :: Templates
mempty = [Template] -> Templates
TExprs [] 

instance PPrint Templates where
  pprintTidy :: Tidy -> Templates -> Doc
pprintTidy Tidy
_ = String -> Doc
text (String -> Doc) -> (Templates -> String) -> Templates -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Templates -> String
forall a. Show a => a -> String
show