rest-rewrite-0.4.4: Rewriting library with online termination checking
Safe HaskellSafe-Inferred
LanguageHaskell2010

Language.REST.Internal.Rewrite

Synopsis

Documentation

data Rewrite Source #

Rewrite t u s defines a rewrite rule \( t \rightarrow u \), with an optional name s.

Constructors

Rewrite MetaTerm MetaTerm (Maybe String) 

Instances

Instances details
Generic Rewrite Source # 
Instance details

Defined in Language.REST.Internal.Rewrite

Associated Types

type Rep Rewrite 
Instance details

Defined in Language.REST.Internal.Rewrite

type Rep Rewrite = D1 ('MetaData "Rewrite" "Language.REST.Internal.Rewrite" "rest-rewrite-0.4.4-A53K0Fl2ieA4Eel1rqijsb" 'False) (C1 ('MetaCons "Rewrite" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaTerm) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaTerm) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)))))

Methods

from :: Rewrite -> Rep Rewrite x #

to :: Rep Rewrite x -> Rewrite #

Show Rewrite Source # 
Instance details

Defined in Language.REST.Internal.Rewrite

Methods

showsPrec :: Int -> Rewrite -> ShowS #

show :: Rewrite -> String #

showList :: [Rewrite] -> ShowS #

Eq Rewrite Source # 
Instance details

Defined in Language.REST.Internal.Rewrite

Methods

(==) :: Rewrite -> Rewrite -> Bool #

(/=) :: Rewrite -> Rewrite -> Bool #

Ord Rewrite Source # 
Instance details

Defined in Language.REST.Internal.Rewrite

Methods

compare :: Rewrite -> Rewrite -> Ordering #

(<) :: Rewrite -> Rewrite -> Bool #

(<=) :: Rewrite -> Rewrite -> Bool #

(>) :: Rewrite -> Rewrite -> Bool #

(>=) :: Rewrite -> Rewrite -> Bool #

max :: Rewrite -> Rewrite -> Rewrite #

min :: Rewrite -> Rewrite -> Rewrite #

Hashable Rewrite Source # 
Instance details

Defined in Language.REST.Internal.Rewrite

Methods

hashWithSalt :: Int -> Rewrite -> Int #

hash :: Rewrite -> Int #

Monad m => RewriteRule m Rewrite RuntimeTerm Source # 
Instance details

Defined in Language.REST.Internal.Rewrite

Methods

apply :: RuntimeTerm -> Rewrite -> m (HashSet RuntimeTerm) Source #

type Rep Rewrite Source # 
Instance details

Defined in Language.REST.Internal.Rewrite

type Rep Rewrite = D1 ('MetaData "Rewrite" "Language.REST.Internal.Rewrite" "rest-rewrite-0.4.4-A53K0Fl2ieA4Eel1rqijsb" 'False) (C1 ('MetaCons "Rewrite" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaTerm) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaTerm) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)))))

type Subst = HashMap String RuntimeTerm Source #

Subst is a mapping from variable names to RuntimeTerms. Normally this would be generated by unifying the left-hand-side of a Rewrite with a term.

named :: Rewrite -> String -> Rewrite Source #

named r n assigns the name n to rule r, replacing any existing name

subst :: Subst -> MetaTerm -> RuntimeTerm Source #

subst s m replaces the variables in the MetaTerm m with RuntimeTerms in the substitution s. This function returns an error if any variables in m do not have a substituion

unify :: MetaTerm -> RuntimeTerm -> Subst -> Maybe Subst Source #

unify m r su extends the substitution su to generate a new substitution that unifies m and r. Returns Nothing if su cannot be extended to unify the terms.