{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} module Language.REST.Internal.Rewrite where import GHC.Generics (Generic) import Data.Hashable import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S import Text.Printf import Language.REST.RewriteRule import Language.REST.MetaTerm as MT import Language.REST.RuntimeTerm data Rewrite = Rewrite MetaTerm MetaTerm (Maybe String) deriving (Rewrite -> Rewrite -> Bool (Rewrite -> Rewrite -> Bool) -> (Rewrite -> Rewrite -> Bool) -> Eq Rewrite forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: Rewrite -> Rewrite -> Bool $c/= :: Rewrite -> Rewrite -> Bool == :: Rewrite -> Rewrite -> Bool $c== :: Rewrite -> Rewrite -> Bool Eq, Eq Rewrite Eq Rewrite -> (Rewrite -> Rewrite -> Ordering) -> (Rewrite -> Rewrite -> Bool) -> (Rewrite -> Rewrite -> Bool) -> (Rewrite -> Rewrite -> Bool) -> (Rewrite -> Rewrite -> Bool) -> (Rewrite -> Rewrite -> Rewrite) -> (Rewrite -> Rewrite -> Rewrite) -> Ord Rewrite Rewrite -> Rewrite -> Bool Rewrite -> Rewrite -> Ordering Rewrite -> Rewrite -> Rewrite forall a. Eq a -> (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: Rewrite -> Rewrite -> Rewrite $cmin :: Rewrite -> Rewrite -> Rewrite max :: Rewrite -> Rewrite -> Rewrite $cmax :: Rewrite -> Rewrite -> Rewrite >= :: Rewrite -> Rewrite -> Bool $c>= :: Rewrite -> Rewrite -> Bool > :: Rewrite -> Rewrite -> Bool $c> :: Rewrite -> Rewrite -> Bool <= :: Rewrite -> Rewrite -> Bool $c<= :: Rewrite -> Rewrite -> Bool < :: Rewrite -> Rewrite -> Bool $c< :: Rewrite -> Rewrite -> Bool compare :: Rewrite -> Rewrite -> Ordering $ccompare :: Rewrite -> Rewrite -> Ordering $cp1Ord :: Eq Rewrite Ord, (forall x. Rewrite -> Rep Rewrite x) -> (forall x. Rep Rewrite x -> Rewrite) -> Generic Rewrite forall x. Rep Rewrite x -> Rewrite forall x. Rewrite -> Rep Rewrite x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a $cto :: forall x. Rep Rewrite x -> Rewrite $cfrom :: forall x. Rewrite -> Rep Rewrite x Generic, Int -> Rewrite -> Int Rewrite -> Int (Int -> Rewrite -> Int) -> (Rewrite -> Int) -> Hashable Rewrite forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a hash :: Rewrite -> Int $chash :: Rewrite -> Int hashWithSalt :: Int -> Rewrite -> Int $chashWithSalt :: Int -> Rewrite -> Int Hashable, Int -> Rewrite -> ShowS [Rewrite] -> ShowS Rewrite -> String (Int -> Rewrite -> ShowS) -> (Rewrite -> String) -> ([Rewrite] -> ShowS) -> Show Rewrite forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Rewrite] -> ShowS $cshowList :: [Rewrite] -> ShowS show :: Rewrite -> String $cshow :: Rewrite -> String showsPrec :: Int -> Rewrite -> ShowS $cshowsPrec :: Int -> Rewrite -> ShowS Show) type Subst = M.HashMap String RuntimeTerm getName :: Rewrite -> Maybe String getName :: Rewrite -> Maybe String getName (Rewrite MetaTerm _t MetaTerm _u Maybe String n) = Maybe String n named :: Rewrite -> String -> Rewrite named :: Rewrite -> String -> Rewrite named (Rewrite MetaTerm t MetaTerm u Maybe String _) String n = MetaTerm -> MetaTerm -> Maybe String -> Rewrite Rewrite MetaTerm t MetaTerm u (String -> Maybe String forall a. a -> Maybe a Just String n) subst :: Subst -> MetaTerm -> RuntimeTerm subst :: Subst -> MetaTerm -> RuntimeTerm subst Subst s (MT.Var String v) | Just RuntimeTerm t <- String -> Subst -> Maybe RuntimeTerm forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v M.lookup String v Subst s = RuntimeTerm t | Bool otherwise = String -> RuntimeTerm forall a. HasCallStack => String -> a error (String -> RuntimeTerm) -> String -> RuntimeTerm forall a b. (a -> b) -> a -> b $ String -> String -> ShowS forall r. PrintfType r => String -> r printf String "No value for metavar %s during subst %s" (ShowS forall a. Show a => a -> String show String v) (Subst -> String forall a. Show a => a -> String show Subst s) subst Subst s (MT.RWApp Op op [MetaTerm] xs) = Op -> [RuntimeTerm] -> RuntimeTerm App Op op ((MetaTerm -> RuntimeTerm) -> [MetaTerm] -> [RuntimeTerm] forall a b. (a -> b) -> [a] -> [b] map (Subst -> MetaTerm -> RuntimeTerm subst Subst s) [MetaTerm] xs) unifyAll :: Subst -> [(MetaTerm, RuntimeTerm)] -> Maybe Subst unifyAll :: Subst -> [(MetaTerm, RuntimeTerm)] -> Maybe Subst unifyAll Subst su [] = Subst -> Maybe Subst forall a. a -> Maybe a Just Subst su unifyAll Subst su ((MetaTerm x, RuntimeTerm y) : [(MetaTerm, RuntimeTerm)] ts) | Just Subst s <- MetaTerm -> RuntimeTerm -> Subst -> Maybe Subst unify MetaTerm x RuntimeTerm y Subst su = Subst -> [(MetaTerm, RuntimeTerm)] -> Maybe Subst unifyAll Subst s [(MetaTerm, RuntimeTerm)] ts | Bool otherwise = Maybe Subst forall a. Maybe a Nothing unify :: MetaTerm -> RuntimeTerm -> Subst -> Maybe Subst unify :: MetaTerm -> RuntimeTerm -> Subst -> Maybe Subst unify (MT.Var String s) RuntimeTerm term Subst su | String -> Subst -> Maybe RuntimeTerm forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v M.lookup String s Subst su Maybe RuntimeTerm -> Maybe RuntimeTerm -> Bool forall a. Eq a => a -> a -> Bool == RuntimeTerm -> Maybe RuntimeTerm forall a. a -> Maybe a Just RuntimeTerm term = Subst -> Maybe Subst forall a. a -> Maybe a Just Subst su unify (MT.Var String s) RuntimeTerm term Subst su | String -> Subst -> Maybe RuntimeTerm forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v M.lookup String s Subst su Maybe RuntimeTerm -> Maybe RuntimeTerm -> Bool forall a. Eq a => a -> a -> Bool == Maybe RuntimeTerm forall a. Maybe a Nothing = Subst -> Maybe Subst forall a. a -> Maybe a Just (Subst -> Maybe Subst) -> Subst -> Maybe Subst forall a b. (a -> b) -> a -> b $ String -> RuntimeTerm -> Subst -> Subst forall k v. (Eq k, Hashable k) => k -> v -> HashMap k v -> HashMap k v M.insert String s RuntimeTerm term Subst su unify (MT.RWApp Op o1 [MetaTerm] xs) (App Op o2 [RuntimeTerm] ys) Subst su | Op o1 Op -> Op -> Bool forall a. Eq a => a -> a -> Bool == Op o2 Bool -> Bool -> Bool && [MetaTerm] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length [MetaTerm] xs Int -> Int -> Bool forall a. Eq a => a -> a -> Bool == [RuntimeTerm] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length [RuntimeTerm] ys = Subst -> [(MetaTerm, RuntimeTerm)] -> Maybe Subst unifyAll Subst su ([MetaTerm] -> [RuntimeTerm] -> [(MetaTerm, RuntimeTerm)] forall a b. [a] -> [b] -> [(a, b)] zip [MetaTerm] xs [RuntimeTerm] ys) unify MetaTerm _ RuntimeTerm _ Subst _ = Maybe Subst forall a. Maybe a Nothing instance Monad m => RewriteRule m Rewrite RuntimeTerm where apply :: RuntimeTerm -> Rewrite -> m (HashSet RuntimeTerm) apply RuntimeTerm t (Rewrite MetaTerm left MetaTerm right Maybe String _) = HashSet RuntimeTerm -> m (HashSet RuntimeTerm) forall (m :: * -> *) a. Monad m => a -> m a return (HashSet RuntimeTerm -> m (HashSet RuntimeTerm)) -> HashSet RuntimeTerm -> m (HashSet RuntimeTerm) forall a b. (a -> b) -> a -> b $ [HashSet RuntimeTerm] -> HashSet RuntimeTerm forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a S.unions ([HashSet RuntimeTerm] -> HashSet RuntimeTerm) -> [HashSet RuntimeTerm] -> HashSet RuntimeTerm forall a b. (a -> b) -> a -> b $ ((RuntimeTerm, RuntimeTerm -> RuntimeTerm) -> HashSet RuntimeTerm) -> [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)] -> [HashSet RuntimeTerm] forall a b. (a -> b) -> [a] -> [b] map (RuntimeTerm, RuntimeTerm -> RuntimeTerm) -> HashSet RuntimeTerm forall a. Hashable a => (RuntimeTerm, RuntimeTerm -> a) -> HashSet a go (RuntimeTerm -> [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)] subTerms RuntimeTerm t) where go :: (RuntimeTerm, RuntimeTerm -> a) -> HashSet a go (RuntimeTerm t', RuntimeTerm -> a tf) | Just Subst su <- MetaTerm -> RuntimeTerm -> Subst -> Maybe Subst unify MetaTerm left RuntimeTerm t' Subst forall k v. HashMap k v M.empty = a -> HashSet a forall a. Hashable a => a -> HashSet a S.singleton (RuntimeTerm -> a tf (RuntimeTerm -> a) -> RuntimeTerm -> a forall a b. (a -> b) -> a -> b $ Subst -> MetaTerm -> RuntimeTerm subst Subst su MetaTerm right) go (RuntimeTerm, RuntimeTerm -> a) _ | Bool otherwise = HashSet a forall a. HashSet a S.empty