Pattern.hs

{-# LANGUAGE QuantifiedConstraints, RankNTypes, UnicodeSyntax, UndecidableInstances #-}
{-|
   Definition of 'Pattern' for use in equality matching
   ('Data.Equality.Matching'), where patterns are matched against the e-graph
 -}
module Data.Equality.Matching.Pattern where

import Data.String

-- | A pattern can be either a variable or an non-variable expression of
-- patterns.
--
-- A 'NonVariablePattern' will only match an expression if the @lang@ constructor matches an expression and all child patterns match the expression children.
-- A 'VariablePattern' matches any expression.
--
-- === Example
--
-- The expression
--
-- @
-- expr :: Fix Sym
-- expr = BinOp Add (Sym "x") (Const 2.0) -- i.e. x + 2
-- @
--
-- Would be matched against the following patterns
--
-- @
-- pat1 :: Pattern Sym
-- pat1 = VariablePattern 1
--
-- pat2 :: Pattern Sym
-- pat2 = NonVariablePattern (BinOp Add (VariablePattern 1) (VariablePattern 2))
--
-- pat3 :: Pattern Sym
-- pat3 = NonVariablePattern (BinOp Add (VariablePattern 1) (NonVariablePattern (Const 2)))
-- @
--
-- But would not be matched against the following patterns
-- 
-- @
-- pat4 :: Pattern Sym
-- pat4 = NonVariablePattern (Const 5)
--
-- pat5 :: Pattern Sym
-- pat5 = NonVariablePattern (BinOp Add (NonVariablePattern (Sym "y")) (NonVariablePattern (Const 2)))
--
-- pat6 :: Pattern Sym
-- pat6 = NonVariablePattern (BinOp Add (NonVariablePattern (Sym "x")) (NonVariablePattern (Const 3)))
-- @
--
-- === IsString
-- 'Pattern' instances 'IsString', which means one can write a variable pattern simply as a string.
--
-- It works by using 'Data.Equality.Utils.hashString' to create a unique integer for a 'VariablePattern'
--
-- For example, we could write the following pattern that would match @a+a@ and @b+b@ but not @a+b@
--
-- @
-- pat7 :: Pattern Sym
-- pat7 = 'pat' (BinOp Add "x" "x")
-- @
data Pattern lang
    = NonVariablePattern (lang (Pattern lang))
    | VariablePattern String

-- | Synonym for 'NonVariablePattern'.
--
-- Example
--
-- @
-- pat8 :: Pattern Sym
-- pat8 = pat (BinOp Mul "y" (pat (Const 2))) -- matches any product of an expression by 2
-- @
pat :: lang (Pattern lang) -> Pattern lang
pat = NonVariablePattern

instance (∀ a. Eq a => Eq (l a)) => (Eq (Pattern l)) where
    (==) (NonVariablePattern a) (NonVariablePattern b) = (==) a b
    (==) (VariablePattern a) (VariablePattern b) = a == b 
    (==) _ _ = False

instance (∀ a. Eq a => Eq (l a), ∀ a. (Ord a) => Ord (l a)) => (Ord (Pattern l)) where
    compare (VariablePattern _) (NonVariablePattern _) = LT
    compare (NonVariablePattern _) (VariablePattern _) = GT
    compare (VariablePattern a) (VariablePattern b) = compare a b
    compare (NonVariablePattern a) (NonVariablePattern b) = compare a b

instance (∀ a. Show a => Show (lang a)) => Show (Pattern lang) where
    showsPrec _ (VariablePattern s) = showString (show s) -- ROMES:TODO don't ignore prec?
    showsPrec d (NonVariablePattern x) = showsPrec d x

instance IsString (Pattern lang) where
    fromString = VariablePattern