diff --git a/rest-rewrite.cabal b/rest-rewrite.cabal --- a/rest-rewrite.cabal +++ b/rest-rewrite.cabal @@ -1,7 +1,7 @@ name: rest-rewrite build-type: Simple -version: 0.1.1 -cabal-version: 1.22 +version: 0.2.0 +cabal-version: 2.0 category: Rewriting maintainer: Zack Grannan author: Zack Grannan @@ -18,35 +18,36 @@ default-language: Haskell2010 exposed-modules: Language.REST - Language.REST.AbstractOC Language.REST.Core + Language.REST.Dot Language.REST.ExploredTerms + Language.REST.Internal.EquivalenceClass + Language.REST.Internal.MultiSet + Language.REST.Internal.MultisetOrder + Language.REST.Internal.OpOrdering + Language.REST.Internal.PartialOrder + Language.REST.Internal.Rewrite + Language.REST.Internal.Util + Language.REST.Internal.WorkStrategy + Language.REST.Internal.WQO + Language.REST.KBO + Language.REST.LPO Language.REST.MetaTerm - Language.REST.Dot - Language.REST.RESTDot + Language.REST.OCAlgebra + Language.REST.OCToAbstract Language.REST.Op - Language.REST.OrderingConstraints - Language.REST.OrderingConstraints.Strict - Language.REST.OrderingConstraints.Lazy - Language.REST.OrderingConstraints.ADT Language.REST.Path + Language.REST.RESTDot + Language.REST.RPO Language.REST.Rest Language.REST.RewriteRule Language.REST.RuntimeTerm Language.REST.SMT Language.REST.Types - other-modules: - Language.REST.WorkStrategy - Language.REST.EquivalenceClass - Language.REST.MultiSet - Language.REST.MultisetOrder - Language.REST.OCToAbstract - Language.REST.OpOrdering - Language.REST.PartialOrder - Language.REST.Rewrite - Language.REST.RPO - Language.REST.WQO - + Language.REST.WQOConstraints + Language.REST.WQOConstraints.ADT + Language.REST.WQOConstraints.Lazy + Language.REST.WQOConstraints.Strict hs-source-dirs: src build-depends: base >= 4.7 && < 5 , containers >= 0.6.2 && < 0.7 @@ -57,117 +58,79 @@ , unordered-containers >= 0.2.13 && < 0.3 , text >= 1.2.4 && < 1.3 +library testlib + default-language: Haskell2010 + build-depends: base >= 4.7 + , containers + , hashable + , process + , QuickCheck + , rest-rewrite + , parsec + , mtl + , monad-loops >= 0.4.3 && < 0.5 + , unordered-containers >= 0.2.11 + , text >= 1.2.2 + , time >= 1.9.3 && < 1.10 + exposed-modules: + Arith + DSL + Language.REST.ConcreteOC + Language.REST.ProofGen + MultisetOrdering + Nat + Set + + hs-source-dirs: testlib + Test-Suite test-rest default-language: Haskell2010 type: exitcode-stdio-1.0 main-is: Test.hs - hs-source-dirs: test src + hs-source-dirs: test build-depends: base , hashable , containers - , parsec , QuickCheck >= 2.14.2 && < 2.15 , mtl , unordered-containers , text - , process + , rest-rewrite + , testlib other-modules: - Arith - DSL - Language.REST.MultiSet - Language.REST.AbstractOC - Language.REST.Core - Language.REST.EquivalenceClass - Language.REST.ExploredTerms - Language.REST.MetaTerm - Language.REST.MultisetOrder - Language.REST.OCToAbstract - Language.REST.Op - Language.REST.OpOrdering - Language.REST.OrderingConstraints - Language.REST.OrderingConstraints.ADT - Language.REST.OrderingConstraints.Lazy - Language.REST.OrderingConstraints.Strict - Language.REST.PartialOrder - Language.REST.Path - Language.REST.RPO - Language.REST.Rest - Language.REST.Rewrite - Language.REST.RewriteRule - Language.REST.RuntimeTerm - Language.REST.Types - Language.REST.WorkStrategy - Language.REST.WQO - Language.REST.SMT + KBO + LazyOC MultisetOrder - Nat OpOrdering QuickCheckTests RPO - Set + SMT StrictOC WQO - - -executable rest +Test-Suite rest default-language: Haskell2010 + type: exitcode-stdio-1.0 main-is: Main.hs -- ghc-plugins: -fplugin=LiquidHaskell build-depends: base >= 4.7 , containers , hashable - , process - , QuickCheck - , parsec + , rest-rewrite , mtl - , monad-loops >= 0.4.3 && < 0.5 , unordered-containers >= 0.2.11 + , testlib , text >= 1.2.2 , time >= 1.9.3 && < 1.10 -- , liquidhaskell -- , liquid-base other-modules: - Arith BagExample Compiler - DSL Group - Language.REST.AbstractOC - Language.REST.ConcreteOC - Language.REST.Core - Language.REST.Dot - Language.REST.EquivalenceClass - Language.REST.ExploredTerms - Language.REST.MetaTerm - Language.REST.MultiSet - Language.REST.MultisetOrder - Language.REST.OCToAbstract - Language.REST.Op - Language.REST.OpOrdering - Language.REST.OrderingConstraints - Language.REST.OrderingConstraints.ADT - Language.REST.OrderingConstraints.Lazy - Language.REST.OrderingConstraints.Strict - Language.REST.PartialOrder - Language.REST.Path - Language.REST.ProofGen - Language.REST.RESTDot - Language.REST.RPO - Language.REST.Rest - Language.REST.Rewrite - Language.REST.RewriteRule - Language.REST.RuntimeTerm - Language.REST.SMT - Language.REST.Types - Language.REST.WQO - Language.REST.WorkStrategy Lists Multiset - MultisetOrdering - Nat NonTerm - Set WQODot - hs-source-dirs: src + hs-source-dirs: test diff --git a/src/Arith.hs b/src/Arith.hs deleted file mode 100644 --- a/src/Arith.hs +++ /dev/null @@ -1,41 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -module Arith where - -import Data.Text -import DSL -import Language.REST.MetaTerm -import Language.REST.Op - -import qualified Data.HashSet as S - -neg x = RWApp (Op "neg") [x] -double x = RWApp (Op "double") [x] -twicePlus x y = RWApp (Op "twicePlus") [x, y] - -evalRWs = - S.fromList - [ (suc' x) #+ y ~> suc' (x #+ y) - , zero' #+ x ~> x - - , (suc' x) #* y ~> y #+ (x #* y) - , zero' #* y ~> zero' - - , ack' zero' x ~> suc' x - , ack' (suc' x) zero' ~> ack' x one' - , ack' (suc' x) (suc' y) ~> ack' x (ack' (suc' x) y) - , double x ~> x #+ x - , twicePlus x y ~> (x #+ x) #+ y - ] - -userRWs = - S.fromList $ - [ x #+ y ~> y #+ x - - , x #* y ~> y #* x - - , (x #+ y) #* v ~> (x #* v) #+ (y #* v) - , (neg x) #+ x ~> zero' - -- , (x #* v) #+ (y #* v) ~> (x #+ y) #* v - - -- , x ~> x #+ zero' - ] ++ [ x #+ (y #+ v) ~> (x #+ y) #+ v] diff --git a/src/BagExample.hs b/src/BagExample.hs deleted file mode 100644 --- a/src/BagExample.hs +++ /dev/null @@ -1,114 +0,0 @@ -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE ImplicitParams #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE TypeSynonymInstances #-} - -module BagExample (mkBagGraph) where - -import Prelude hiding (EQ, GT) - - -import Control.Monad.Identity -import Language.REST.Dot -import Language.REST.RESTDot -import Language.REST.OCToAbstract -import Language.REST.RewriteRule -import qualified Language.REST.MultiSet as M -import Language.REST.MultisetOrder -import Language.REST.Rest -import Language.REST.OrderingConstraints as OC -import Language.REST.OrderingConstraints.Strict as SC -import Language.REST.WQO as WQO -import Language.REST.WorkStrategy -import Language.REST.Types -import Language.REST.SMT - -import qualified Data.List as L -import qualified Data.HashSet as S -import qualified Data.Text as T -import GHC.Generics (Generic) -import Data.Hashable - -data PChar = PChar Char deriving (Eq, Ord, Generic, Hashable) - -instance ToSMTVar PChar Int where - toSMTVar c = SMTVar $ T.pack $ "char_" ++ show c - -instance Show PChar where - show (PChar c) = return c - -data Bag = Bag String - deriving (Eq, Ord, Generic, Hashable) - -instance Show Bag where - show = showBag - - -toMultiset :: Bag -> M.MultiSet PChar -toMultiset (Bag str) = M.fromList $ map PChar str - - -bag :: String -> Bag -bag = Bag - -data Rewrite = Rewrite Bag (S.HashSet Bag) - deriving (Eq, Ord, Generic, Hashable) - -infixr 1 ~> -(~>) = (:) - -instance RewriteRule IO Rewrite Bag where - apply bag (Rewrite bag' result) | bag == bag' = return result - apply _ _ | otherwise = return S.empty - - -fromPath :: [String] -> S.HashSet Rewrite -fromPath [] = S.empty -fromPath xs = S.fromList $ map go (zip xs (tail xs)) - where - go :: (String, String) -> Rewrite - go (x, y) = Rewrite (bag x) (S.singleton $ bag y) - - -fromPaths :: [[String]] -> S.HashSet Rewrite -fromPaths paths = S.unions $ map fromPath paths - -start = "AAB" - -rules :: S.HashSet Rewrite -rules = fromPaths $ - [ start ~> "ACD" ~> "AAAA" ~> "ABDD" ~> [] - , start ~> "ABD" ~> "AB" ~> "BBD" ~> [] - ] - -showBag :: Bag -> String -showBag (Bag bag) = "{ " ++ (L.intercalate ", " $ map return bag) ++ " }" - -showRule :: Rewrite -> String -showRule _ = "" - - -compareChar :: ConstraintGen impl PChar PChar Identity -compareChar impl GTE oc c1 c2 | c1 /= c2 = compareChar impl GT oc c1 c2 -compareChar impl EQ _ c1 c2 | c1 /= c2 = return $ OC.unsatisfiable impl -compareChar impl r oc c1 c2 = return $ intersectRelation impl oc (c1, c2, r) - - -mkBagGraph = - do - (PathsResult paths, _) <- rest - RESTParams - { re = S.empty - , ru = rules - , toET = id - , target = Nothing - , workStrategy = bfs - , ocImpl = impl - , initRes = pathsResult - } (bag start) - let prettyPrinter = PrettyPrinter showRule showBag show True - writeDot "example" Tree prettyPrinter (toOrderedSet paths) - where - impl = lift SC.strictOC $ cmapConstraints toMultiset (multisetOrder compareChar) diff --git a/src/Compiler.hs b/src/Compiler.hs deleted file mode 100644 --- a/src/Compiler.hs +++ /dev/null @@ -1,29 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -module Compiler where - -import Data.Text -import qualified Arith as A -import DSL -import Language.REST.MetaTerm -import Language.REST.Op - -import qualified Data.HashSet as S -import Prelude hiding (repeat, seq) - -repeat n op = RWApp (Op "repeat") [n, op] -seq op1 op2 = RWApp (Op "seq") [op1, op2] -nop = RWApp (Op "nop") [] - - -userRWs = - S.union A.userRWs - (S.fromList $ [ - seq x nop ~> x - , seq nop x ~> x - , repeat zero' x ~> nop - ] ++ (repeat (suc' y) x <~> seq x (repeat y x)) - -- ++ (repeat (suc' y) x <~> seq (repeat y x) x) - ++ (repeat (suc' (suc' zero')) x <~> seq x x)) - -evalRWs = S.empty -- S.fromList [ ] diff --git a/src/DSL.hs b/src/DSL.hs deleted file mode 100644 --- a/src/DSL.hs +++ /dev/null @@ -1,77 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -module DSL where - -import Language.REST.Op -import qualified Language.REST.MetaTerm as MT -import Language.REST.RuntimeTerm as RT -import Language.REST.Rewrite -import Nat - -type MetaTerm = MT.MetaTerm - -commutes op = x `op` y ~> y `op` x -assocL op = (x `op` y) `op` z' ~> x `op` (y `op` z') -assocR op = x `op` (y `op` z') ~> (x `op` y) `op` z' -distribL op1 op2 = (x `op1` y) `op2` z' ~> (x `op2` z') `op1` (y `op2` z') -distribR op1 op2 = z' `op2` (x `op1` y) ~> (z' `op2` x) `op1` (z' `op2` y) - -ackOp = Op "ack" -plus = Op "+" -minus = Op "-" -times = Op "*" - -a = App (Op "a") [] -b = App (Op "b") [] -c = App (Op "c") [] -d = App (Op "d") [] -x = MT.Var "x" -y = MT.Var "y" -v = MT.Var "v" -w = MT.Var "w" -z' = MT.Var "z" - -f = Op "f" -g = Op "g" -h = Op "h" - -t1Op = Op "t1" -t2Op = Op "t2" - -t1 = App (Op "t1") [] -t2 = App (Op "t2") [] -t3 = App (Op "t3") [] -t4 = App (Op "t4") [] -t5 = App (Op "t5") [] - -zero = App z [] -one = suc zero -two = suc one -suc x = App s [x] -ack x y = App ackOp [x, y] - -zero' = MT.toMetaTerm zero -one' = suc' zero' -suc' x = MT.RWApp s [x] -ack' x y = MT.RWApp ackOp [x, y] - -infixl 1 .+ -(.+) :: RuntimeTerm -> RuntimeTerm -> RuntimeTerm -(.+) x y = App plus [x, y] - -(#+) :: MetaTerm -> MetaTerm -> MetaTerm -(#+) x y = MT.RWApp plus [x, y] - -(#-) :: MetaTerm -> MetaTerm -> MetaTerm -(#-) x y = MT.RWApp minus [x, y] - -(#*) :: MetaTerm -> MetaTerm -> MetaTerm -(#*) x y = MT.RWApp times [x, y] - -infix 0 ~> -(~>) :: MetaTerm -> MetaTerm -> Rewrite -t ~> u = Rewrite t u Nothing - -infix 0 <~> -(<~>) :: MetaTerm -> MetaTerm -> [Rewrite] -t <~> u = [ t ~> u, u ~> t ] diff --git a/src/Group.hs b/src/Group.hs deleted file mode 100644 --- a/src/Group.hs +++ /dev/null @@ -1,23 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -module Group where - -import Data.Text -import DSL -import Language.REST.Op -import Language.REST.MetaTerm - -import qualified Data.HashSet as S - -neg x = RWApp (Op "neg") [x] - -evalRWs = S.empty - -userRWs = - S.fromList - [ - x #+ zero' ~> x - , zero' #+ x ~> x - , (neg x) #+ x ~> zero' - , (x #+ y) #+ v ~> x #+ (y #+ v) - ] diff --git a/src/Language/REST.hs b/src/Language/REST.hs --- a/src/Language/REST.hs +++ b/src/Language/REST.hs @@ -6,21 +6,20 @@ import Data.Hashable import Data.Maybe import qualified Data.HashSet as S -import qualified Data.HashMap.Strict as M -import Language.REST.Types +import Language.REST.OCAlgebra (OCAlgebra) import Language.REST.OCToAbstract -import Language.REST.OrderingConstraints -import Language.REST.OrderingConstraints.Strict (strictOC) -import Language.REST.OrderingConstraints.Lazy (lazyOC) -import Language.REST.OrderingConstraints.ADT (adtOC) +import Language.REST.WQOConstraints +import Language.REST.WQOConstraints.ADT (ConstraintsADT, adtOC) import Language.REST.RPO import Language.REST.RuntimeTerm import Language.REST.Op -import Language.REST.OpOrdering -import qualified Language.REST.WQO as WQO +import Language.REST.Internal.OpOrdering +import qualified Language.REST.Internal.WQO as WQO +import System.IO (Handle) +adtRPO :: (Handle, Handle) -> OCAlgebra (ConstraintsADT Op) RuntimeTerm IO adtRPO z3 = lift (adtOC z3) rpo -- lazyRPO = lift lazyOC rpo -- strictRPO = lift strictOC rpo @@ -28,7 +27,7 @@ -- Assume vars are arity 0, which is usually correct getVars :: RuntimeTerm -> S.HashSet Op getVars (App op []) = S.singleton op -getVars (App op xs) = S.unions (map getVars xs) +getVars (App _op xs) = S.unions (map getVars xs) varsEQ :: RuntimeTerm -> RuntimeTerm -> WQO.WQO Op diff --git a/src/Language/REST/AbstractOC.hs b/src/Language/REST/AbstractOC.hs deleted file mode 100644 --- a/src/Language/REST/AbstractOC.hs +++ /dev/null @@ -1,32 +0,0 @@ -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -module Language.REST.AbstractOC where - -data AbstractOC c a m = AbstractOC - { - isSat :: c -> m Bool - , refine :: c -> a -> a -> c - , top :: c - - -- For explore optimizations, if not required just make it return 2nd param - , union :: c -> c -> c - -- If not required return False - , notStrongerThan :: c -> c -> m Bool - } - -fuelOC :: (Monad m) => Int -> AbstractOC Int a m -fuelOC initFuel = AbstractOC isSat' refine' initFuel union' notStrongerThan' - where - isSat' c = return $ c >= 0 - refine' c _ _ = c - 1 - union' c c' = max c c' - notStrongerThan' c c' = return $ c >= c' - -contramap :: forall c a b m . - (b -> a) - -> AbstractOC c a m - -> AbstractOC c b m -contramap f aoc = aoc{refine = refine'} - where - refine' :: c -> b -> b -> c - refine' c t1 t2 = refine aoc c (f t1) (f t2) diff --git a/src/Language/REST/ConcreteOC.hs b/src/Language/REST/ConcreteOC.hs deleted file mode 100644 --- a/src/Language/REST/ConcreteOC.hs +++ /dev/null @@ -1,57 +0,0 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DeriveGeneric #-} - -module Language.REST.ConcreteOC where - -import qualified Language.REST.AbstractOC as AOC -import qualified Language.REST.WQO as WQO -import Language.REST.RuntimeTerm -import Language.REST.RPO -import Language.REST.OpOrdering -import Language.REST.MetaTerm - -import Data.List as L -import Data.Hashable -import GHC.Generics (Generic) -import qualified Data.Set as S - -data ConcreteOC = ConcreteOC [RuntimeTerm] (Maybe OpOrdering) - deriving (Eq, Ord, Generic, Hashable) - -instance Show ConcreteOC where - show (ConcreteOC _ (Just oo)) = show oo - show _ = "impossible" - -isSat (ConcreteOC _ (Just _)) = True -isSat _ = False - -getOrdering ts = - let - ops = S.unions $ map termOps ts - orderings = S.toList $ WQO.orderings ops - in - L.find (`orients` ts) orderings - - -orients :: OpOrdering -> [RuntimeTerm] -> Bool -orients ordering terms = - let - pairs = zip terms (tail terms) - in - all (uncurry $ synGTE ordering) pairs - -concreteOC :: Monad m => AOC.AbstractOC ConcreteOC RuntimeTerm m -concreteOC = AOC.AbstractOC (return . isSat) refine (ConcreteOC [] (Just (WQO.empty))) union notStrongerThan - where - union t1 _ = t1 - notStrongerThan _ _ = return False - refine :: ConcreteOC -> RuntimeTerm -> RuntimeTerm -> ConcreteOC - refine (ConcreteOC ts (Just o)) _ u = - let - ts' = ts ++ [u] - in - ConcreteOC ts' $ - if o `orients` ts' - then Just o - else getOrdering ts' - refine (ConcreteOC ts Nothing) _ u = ConcreteOC (ts ++ [u]) Nothing diff --git a/src/Language/REST/Core.hs b/src/Language/REST/Core.hs --- a/src/Language/REST/Core.hs +++ b/src/Language/REST/Core.hs @@ -8,19 +8,13 @@ import Prelude hiding (GT, EQ) import Debug.Trace ( trace ) -import Data.Functor.Identity import qualified Data.List as L import qualified Data.HashSet as S -import Language.REST.AbstractOC -import Language.REST.Op -import Language.REST.OrderingConstraints -import Language.REST.RPO -import Language.REST.OpOrdering as OO +import Language.REST.OCAlgebra import Language.REST.Types import qualified Language.REST.MetaTerm as MT -import Language.REST.WQO -import Language.REST.Rewrite +import Language.REST.Internal.Rewrite import Language.REST.RuntimeTerm as RT import Language.REST.RewriteRule @@ -32,18 +26,20 @@ contains (App _ ts) t = any (contains t) ts -orient' :: Show oc => (?impl :: AbstractOC oc RuntimeTerm m) => oc -> [RuntimeTerm] -> oc +orient' :: Show oc => (?impl :: OCAlgebra oc RuntimeTerm m) => oc -> [RuntimeTerm] -> oc orient' oc0 ts0 = go oc0 (zip ts0 (tail ts0)) where go oc [] = oc go oc ((t0, t1):ts) = go (refine ?impl oc t0 t1) ts -orient :: Show oc => (?impl :: AbstractOC oc RuntimeTerm m) => [RuntimeTerm] -> oc -orient = orient' (top ?impl) +orient :: Show oc => OCAlgebra oc RuntimeTerm m -> [RuntimeTerm] -> oc +orient impl = orient' (top impl) + where + ?impl = impl canOrient :: forall oc m . Show oc - => (?impl :: AbstractOC oc RuntimeTerm m) => [RuntimeTerm] -> m Bool -canOrient terms = trace ("Try to orient " ++ termPathStr terms) $ isSat ?impl (orient terms) + => (?impl :: OCAlgebra oc RuntimeTerm m) => [RuntimeTerm] -> m Bool +canOrient terms = trace ("Try to orient " ++ termPathStr terms) $ isSat ?impl (orient ?impl terms) syms :: MetaTerm -> S.HashSet String syms (MT.Var s) = S.singleton s @@ -55,9 +51,9 @@ pp = prettyPrint (PPArgs [] [] (const Nothing)) eval :: S.HashSet Rewrite -> RuntimeTerm -> IO RuntimeTerm -eval rws t = +eval rws t0 = do - result <- mapM (apply t) (S.toList rws) + result <- mapM (apply t0) (S.toList rws) case S.toList $ S.unions result of - [] -> return t + [] -> return t0 (t : _) -> eval rws t diff --git a/src/Language/REST/Dot.hs b/src/Language/REST/Dot.hs --- a/src/Language/REST/Dot.hs +++ b/src/Language/REST/Dot.hs @@ -36,25 +36,26 @@ type DotPath = [Node] nodeString :: Node -> String -nodeString (Node id label style color) = - printf "\t%s [label=\"%s\"\nstyle=\"%s\"\ncolor=\"%s\"];" id label style color +nodeString (Node nid elabel style color) = + printf "\t%s [label=\"%s\"\nstyle=\"%s\"\ncolor=\"%s\"];" nid elabel style color edgeString :: Edge -> String -edgeString (Edge from to label color subLabel style) = +edgeString (Edge efrom eto elabel color esubLabel style) = let - sub = escape subLabel + sub = escape esubLabel escape xs = concatMap go xs where go '\\' = "\\" go '\n' = "
" go '>' = ">" + go '<' = "<" go o = [o] labelPart = - if label /= "" - then printf "%s" label + if elabel /= "" + then printf "%s" (escape elabel) else "" in - printf "\t%s -> %s [label = <%s
%s>\ncolor=\"%s\"\nstyle=\"%s\"];" from to labelPart sub color style + printf "\t%s -> %s [label = <%s
%s>\ncolor=\"%s\"\nstyle=\"%s\"];" efrom eto labelPart sub color style graphString :: DiGraph -> String graphString (DiGraph name nodes edges) = diff --git a/src/Language/REST/EquivalenceClass.hs b/src/Language/REST/EquivalenceClass.hs deleted file mode 100644 --- a/src/Language/REST/EquivalenceClass.hs +++ /dev/null @@ -1,73 +0,0 @@ -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveAnyClass #-} - -module Language.REST.EquivalenceClass - ( isMember - , isSingleton - , insert - , union - , singleton - , fromList - , toList - , head - , EquivalenceClass - , elems - , toPairs - , isSubsetOf - ) where - -import GHC.Generics (Generic) -import Data.Hashable -import qualified Data.Set as S -import qualified Data.List as L -import Prelude hiding (head) - -import Language.REST.Types -import Language.REST.SMT - -newtype EquivalenceClass a = - EquivalenceClass (S.Set a) deriving (Ord, Eq, Generic, Hashable) - -instance Show a => Show (EquivalenceClass a) where - show (EquivalenceClass xs) = L.intercalate " = " (map show (S.toList xs)) - - - -{-# INLINE isSubsetOf #-} -isSubsetOf (EquivalenceClass xs) (EquivalenceClass ys) = xs `S.isSubsetOf` ys - -head :: EquivalenceClass a -> a -head (EquivalenceClass xs) = L.head $ S.toList xs - -isSingleton (EquivalenceClass xs) = S.size xs == 1 - -{-# INLINE isMember #-} -isMember :: (Ord a, Eq a, Hashable a) => a -> EquivalenceClass a -> Bool -isMember x (EquivalenceClass xs) = S.member x xs - -insert :: (Ord a, Eq a, Hashable a) => a -> EquivalenceClass a -> EquivalenceClass a -insert x (EquivalenceClass xs) = EquivalenceClass (S.insert x xs) - -union :: (Ord a, Eq a, Hashable a) => EquivalenceClass a -> EquivalenceClass a -> EquivalenceClass a -union (EquivalenceClass xs) (EquivalenceClass ys) = - EquivalenceClass (S.union xs ys) - -singleton :: (Ord a, Eq a, Hashable a) => a -> EquivalenceClass a -singleton = EquivalenceClass . S.singleton - -fromList :: (Ord a, Eq a, Hashable a) => [a] -> EquivalenceClass a -fromList = EquivalenceClass . S.fromList - -toList :: EquivalenceClass a -> [a] -toList (EquivalenceClass s) = S.toList s - -toPairs e = - let - list = toList e - in - if length list < 2 - then [] - else zip list (tail list) - -{-# INLINE elems #-} -elems (EquivalenceClass ec) = ec diff --git a/src/Language/REST/ExploredTerms.hs b/src/Language/REST/ExploredTerms.hs --- a/src/Language/REST/ExploredTerms.hs +++ b/src/Language/REST/ExploredTerms.hs @@ -9,9 +9,9 @@ , size , visited , ExploreFuncs(..) + , ExploreStrategy(..) ) where -import Debug.Trace import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S import Data.Hashable @@ -31,6 +31,7 @@ data ExploredTerms term c m = ET (M.HashMap term (c, (S.HashSet term))) (ExploreFuncs c m) ExploreStrategy +trace' :: String -> b -> b -- trace' = trace trace' _ x = x @@ -38,8 +39,8 @@ size :: ExploredTerms term c m -> Int size (ET m _ _) = M.size m -empty :: ExploreFuncs c m -> ExploredTerms term c m -empty ef = ET M.empty ef ExploreWhenNeeded +empty :: ExploreFuncs c m -> ExploreStrategy -> ExploredTerms term c m +empty = ET M.empty visited :: (Eq term, Hashable term) => term -> ExploredTerms term c m -> Bool visited t (ET m _ _) = M.member t m diff --git a/src/Language/REST/Internal/EquivalenceClass.hs b/src/Language/REST/Internal/EquivalenceClass.hs new file mode 100644 --- /dev/null +++ b/src/Language/REST/Internal/EquivalenceClass.hs @@ -0,0 +1,76 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveAnyClass #-} + +module Language.REST.Internal.EquivalenceClass + ( isMember + , isSingleton + , insert + , union + , singleton + , fromList + , toList + , head + , EquivalenceClass + , elems + , toPairs + , isSubsetOf + ) where + +import GHC.Generics (Generic) +import Data.Hashable +import qualified Data.Set as S +import qualified Data.List as L +import Prelude hiding (head) + +import Language.REST.Types () -- Hashable (S.Set a) + +newtype EquivalenceClass a = + EquivalenceClass (S.Set a) deriving (Ord, Eq, Generic, Hashable) + +instance Show a => Show (EquivalenceClass a) where + show (EquivalenceClass xs) = L.intercalate " = " (map show (S.toList xs)) + + + +{-# INLINE isSubsetOf #-} +isSubsetOf :: Ord a => EquivalenceClass a -> EquivalenceClass a -> Bool +isSubsetOf (EquivalenceClass xs) (EquivalenceClass ys) = xs `S.isSubsetOf` ys + +head :: EquivalenceClass a -> a +head (EquivalenceClass xs) = L.head $ S.toList xs + +isSingleton :: EquivalenceClass a -> Bool +isSingleton (EquivalenceClass xs) = S.size xs == 1 + +{-# INLINE isMember #-} +isMember :: (Ord a, Eq a, Hashable a) => a -> EquivalenceClass a -> Bool +isMember x (EquivalenceClass xs) = S.member x xs + +insert :: (Ord a, Eq a, Hashable a) => a -> EquivalenceClass a -> EquivalenceClass a +insert x (EquivalenceClass xs) = EquivalenceClass (S.insert x xs) + +union :: (Ord a, Eq a, Hashable a) => EquivalenceClass a -> EquivalenceClass a -> EquivalenceClass a +union (EquivalenceClass xs) (EquivalenceClass ys) = + EquivalenceClass (S.union xs ys) + +singleton :: (Ord a, Eq a, Hashable a) => a -> EquivalenceClass a +singleton = EquivalenceClass . S.singleton + +fromList :: (Ord a, Eq a, Hashable a) => [a] -> EquivalenceClass a +fromList = EquivalenceClass . S.fromList + +toList :: EquivalenceClass a -> [a] +toList (EquivalenceClass s) = S.toList s + +toPairs :: EquivalenceClass b -> [(b, b)] +toPairs e = + let + list = toList e + in + if length list < 2 + then [] + else zip list (tail list) + +{-# INLINE elems #-} +elems :: EquivalenceClass a -> S.Set a +elems (EquivalenceClass ec) = ec diff --git a/src/Language/REST/Internal/MultiSet.hs b/src/Language/REST/Internal/MultiSet.hs new file mode 100644 --- /dev/null +++ b/src/Language/REST/Internal/MultiSet.hs @@ -0,0 +1,80 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveAnyClass #-} + +module Language.REST.Internal.MultiSet + ( MultiSet + , delete + , deleteMany + , distinctElems + , empty + , filter + , insert + , member + , null + , toList + , toOccurList + , singleton + , fromList + , toSet + ) where + +import Prelude hiding (null, filter) + +import GHC.Generics +import Data.Hashable +import qualified Data.List as L +import qualified Data.HashMap.Strict as M +import qualified Data.HashSet as S + +data MultiSet a = MultiSet (M.HashMap a Int) deriving (Eq, Generic, Hashable, Ord) + +instance Show a => Show (MultiSet a) where + show ms = "{" ++ L.intercalate ", " (map show $ toList ms) ++ "}" + +delete :: (Hashable a, Eq a) => a -> MultiSet a -> MultiSet a +delete k = deleteMany k 1 + +deleteMany :: (Hashable a, Eq a) => a -> Int -> MultiSet a -> MultiSet a +deleteMany k v (MultiSet ms) | Just c <- M.lookup k ms + , c > v = MultiSet $ M.insert k (c - v) ms +deleteMany k _ (MultiSet ms) | otherwise = MultiSet $ M.delete k ms + +distinctElems :: MultiSet a -> [a] +distinctElems (MultiSet ms) = M.keys ms + +empty :: MultiSet a +empty = MultiSet M.empty + +toOccurList :: MultiSet a -> [(a, Int)] +toOccurList (MultiSet ms) = M.toList ms + +filter :: (a -> Bool) -> MultiSet a -> MultiSet a +filter f (MultiSet ms) = MultiSet $ M.filterWithKey f' ms + where + f' k _ = f k + +null :: MultiSet a -> Bool +null (MultiSet ms) = M.null ms + +member :: (Eq a, Hashable a) => a -> MultiSet a -> Bool +member k (MultiSet ms) = M.member k ms + +toList :: MultiSet a -> [a] +toList ms = concatMap go (toOccurList ms) + where + go (k, num) = take num $ repeat k + +insert :: (Eq a, Hashable a) => a -> MultiSet a -> MultiSet a +insert k (MultiSet ms) | Just c <- M.lookup k ms + = MultiSet $ M.insert k (c + 1) ms +insert k (MultiSet ms) | otherwise + = MultiSet $ M.insert k 1 ms + +singleton :: (Eq a, Hashable a) => a -> MultiSet a +singleton k = MultiSet (M.singleton k 1) + +fromList :: (Eq a, Hashable a) => [a] -> MultiSet a +fromList = foldl (flip insert) empty + +toSet :: MultiSet a -> S.HashSet a +toSet (MultiSet ms) = M.keysSet ms diff --git a/src/Language/REST/Internal/MultisetOrder.hs b/src/Language/REST/Internal/MultisetOrder.hs new file mode 100644 --- /dev/null +++ b/src/Language/REST/Internal/MultisetOrder.hs @@ -0,0 +1,78 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveAnyClass #-} + +module Language.REST.Internal.MultisetOrder (multisetOrder, possibilities) where + +import GHC.Generics +import qualified Data.List as L +import Prelude hiding (EQ, GT) +import Data.Hashable +import qualified Data.HashSet as S + +import qualified Language.REST.Internal.MultiSet as M +import Language.REST.WQOConstraints as OC +import Language.REST.Types + +type MultiSet = M.MultiSet + +trace' :: String -> a -> a +-- trace' = trace +trace' _ x = x + +removeEQs :: (Eq x, Ord x, Hashable x) => MultiSet x -> MultiSet x -> (MultiSet x, MultiSet x) +removeEQs ts0 us0 = go (M.toList ts0) M.empty us0 where + go [] ts us = (ts, us) + go (x : xs) ts us | x `M.member` us = go xs ts (M.delete x us) + go (x : xs) ts us | otherwise = go xs (M.insert x ts) us + +data Replace a = + ReplaceOne a a + | Replace a (S.HashSet a) + deriving (Eq, Hashable, Generic, Show) + +powerset :: [a] -> [[a]] +powerset [] = [[]] +powerset (x:xs) = [x:ps | ps <- powerset xs] ++ powerset xs + +possibilities :: (Hashable a, Eq a) => Relation -> [a] -> [a] -> S.HashSet (S.HashSet (Replace a)) +possibilities r [] [] = if r == GT then S.empty else S.singleton (S.empty) +possibilities r xs [] = if r == EQ then S.empty else S.singleton (S.fromList $ map (flip Replace S.empty) xs) +possibilities _ [] (_:_) = S.empty +possibilities r (x:xs) ys = if r == EQ then eqs else S.union eqs doms where + eqs = S.unions $ map go ys where + go y = S.map (S.insert (ReplaceOne x y)) (possibilities r xs (L.delete y ys)) + doms = S.unions $ map go (powerset $ L.nub ys) where + go ys' = S.map + (S.insert (Replace x (S.fromList ys'))) + (possibilities GTE xs (filter (not . flip elem ys') ys)) + + +multisetOrder :: forall oc base lifted m . (Ord lifted, Ord base, Show base, Eq base, Hashable base, Hashable lifted, Eq lifted, Show (oc base), Eq (oc base), Monad m) => + ConstraintGen oc base lifted m + -> ConstraintGen oc base (MultiSet lifted) m +multisetOrder _ impl _ oc _ _ | oc == unsatisfiable impl = return $ unsatisfiable impl +multisetOrder underlying impl r oc ts0 us0 = (uncurry go) (removeEQs ts0 us0) where + go :: MultiSet lifted -> MultiSet lifted -> m (oc base) + go ts us | M.null ts && M.null us = return $ if r == GT then unsatisfiable impl else oc + go ts us | not (M.null ts) && M.null us = return $ if r == EQ then unsatisfiable impl else oc + go ts us | M.null ts && not (M.null us) = return $ unsatisfiable impl + go ts us = result + where + + pos = possibilities r (M.toList ts) (M.toList us) + + result = + trace' ("There are " ++ (show $ S.size pos) ++ " possibilities") $ + unionAll impl <$> mapM posConstraints (S.toList pos) + + posConstraints pos1 = L.foldl' apply (return oc) (S.toList pos1) where + apply moc (ReplaceOne t u) = do + oc' <- moc + underlying impl EQ oc' t u + apply moc (Replace t ts') = do + oc' <- moc + if S.null ts' + then return oc' + else intersectAll impl <$> (mapM (underlying impl GT oc' t) (S.toList ts')) diff --git a/src/Language/REST/Internal/OpOrdering.hs b/src/Language/REST/Internal/OpOrdering.hs new file mode 100644 --- /dev/null +++ b/src/Language/REST/Internal/OpOrdering.hs @@ -0,0 +1,100 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeSynonymInstances #-} + + +module Language.REST.Internal.OpOrdering ( + empty + , merge + , OpOrdering + , opInsert + , opGT + , opEQ + , (=.) + , (>.) + , (<.) + , parseOO + ) where + +import Prelude hiding (GT, EQ) +import Data.Maybe +import qualified Data.Text as T +import Text.ParserCombinators.Parsec.Char +import Text.ParserCombinators.Parsec +import Text.Parsec (Parsec) + +import Language.REST.Op +import Language.REST.Internal.WQO as WQO + + +type OpOrdering = WQO Op + + +opGT :: OpOrdering -> Op -> Op -> Bool +opGT s f g = getRelation s f g == Just QGT + +opEQ :: OpOrdering -> Op -> Op -> Bool +opEQ s f g = getRelation s f g == Just QEQ + + +opInsert :: OpOrdering -> Op -> Op -> QORelation -> Maybe OpOrdering +opInsert o f g r = + case WQO.insert o (f, g, r) of + ValidExtension o' -> Just o' + _ -> Nothing + +-- The following only are valid if f /= g. + +-- precondition : f /= g +(>.) :: Op -> Op -> OpOrdering +(>.) f g = fromJust $ WQO.singleton (f, g, QGT) + +-- precondition : f /= g +(=.) :: Op -> Op -> OpOrdering +(=.) f g = fromJust $ WQO.singleton (f, g, QEQ) + +-- precondition : f /= g +(<.) :: Op -> Op -> OpOrdering +(<.) f g = g >. f + +parseOO :: String -> Maybe OpOrdering +parseOO str = + case parse parser "" str of + Left err -> error (show err) + Right t -> t + +parser :: Parsec String u (Maybe OpOrdering) +parser = fmap mergeAll' (sepBy1 atom conj) where + + mergeAll' :: [Maybe OpOrdering] -> Maybe OpOrdering + mergeAll' [x] = x + mergeAll' (Just x : Just x' : xs) = + do + x'' <- merge x x' + mergeAll' (Just x'' : xs) + mergeAll' _ = Nothing + + conj = spaces >> (char '\8743' <|> char '^') >> spaces + eq = spaces >> char '=' >> spaces + gt = spaces >> char '>' >> spaces + + + atom = try gtAtom <|> try eqAtom + + eqAtom = fmap allEQ (sepBy1 sym (try eq)) + where + mkEQ f g = WQO.singleton (f, g, QEQ) + allEQ syms = + let + pairs = zipWith mkEQ syms (tail syms) + in + mergeAll' pairs + + gtAtom = do + left <- sym + _ <- gt + right <- sym + return $ WQO.singleton (left, right, QGT) + + sym = fmap (Op . T.pack) (many (alphaNum <|> char '+' <|> char '*')) diff --git a/src/Language/REST/Internal/PartialOrder.hs b/src/Language/REST/Internal/PartialOrder.hs new file mode 100644 --- /dev/null +++ b/src/Language/REST/Internal/PartialOrder.hs @@ -0,0 +1,104 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveAnyClass #-} + +module Language.REST.Internal.PartialOrder ( + empty + , insert + , replaceUnsafe + , insertUnsafe + , gt + , toList + , isEmpty + , elems + , unionDisjointUnsafe + , PartialOrder + , toDescsList + , descendents + ) where + +import GHC.Generics (Generic) +import Data.Hashable +import qualified Data.Set as S +import qualified Data.Map as M +import qualified Data.List as L + +import Language.REST.Types () -- Hashable (M.Map a b) +import Text.Printf + +newtype PartialOrder a = PartialOrder (M.Map a (S.Set a)) + deriving (Ord, Eq, Generic, Hashable) + +instance (Show a) => Show (PartialOrder a) where + show (PartialOrder m) = L.intercalate " ∧ " $ map go (M.toList m) where + go (key, s) = case S.toList s of + [x] -> printf "%s > %s" (show key) (show x) + xs -> printf "%s > { %s }" (show key) (L.intercalate ", " (map show xs)) + +empty :: PartialOrder a +empty = PartialOrder M.empty + +isEmpty :: Eq a => PartialOrder a -> Bool +isEmpty p = p == empty + +canInsert :: (Eq a, Ord a, Hashable a) => PartialOrder a -> a -> a -> Bool +canInsert o f g = f /= g && not (gt o f g) && not (gt o g f) + +gt :: (Eq a, Ord a, Hashable a) => PartialOrder a -> a -> a -> Bool +gt po t u = S.member u $ descendents t po + +unionDisjointUnsafe :: Ord a => PartialOrder a -> PartialOrder a -> PartialOrder a +unionDisjointUnsafe (PartialOrder m) (PartialOrder m') = PartialOrder (M.union m m') + +ascendants :: Ord k => k -> PartialOrder k -> S.Set k +ascendants k (PartialOrder m) = M.keysSet $ M.filter (S.member k) m + +descendents :: Ord a => a -> PartialOrder a -> S.Set a +descendents k (PartialOrder m) = M.findWithDefault S.empty k m + +{-# INLINE insertUnsafe #-} +insertUnsafe :: Ord a => PartialOrder a -> a -> a -> PartialOrder a +insertUnsafe o@(PartialOrder m) f g = result + where + result = PartialOrder $ M.insertWith S.union f decs $ M.mapWithKey go m + + go k old | S.member k ascs = S.union old decs + go _ v | otherwise = v + + ascs = ascendants f o + decs = S.insert g $ descendents g o + +{-# INLINE insert #-} +insert :: (Eq a, Ord a, Hashable a) => PartialOrder a -> a -> a -> Maybe (PartialOrder a) +insert o f g = if canInsert o f g then Just (insertUnsafe o f g) else Nothing + +toDescsList :: PartialOrder k -> [(k, S.Set k)] +toDescsList (PartialOrder m) = M.toList m + +toList :: PartialOrder a -> [(a, a)] +toList (PartialOrder m) = do + (k, vs) <- M.toList m + v <- S.toList vs + return (k, v) + +elems :: (Eq a, Ord a, Hashable a) => PartialOrder a -> S.Set a +elems (PartialOrder m) = S.union (M.keysSet m) (S.unions (M.elems m)) + +replaceUnsafe :: (Eq a, Ord a, Hashable a) => [a] -> a -> PartialOrder a -> PartialOrder a +replaceUnsafe froms to po@(PartialOrder m) = result where + + from' = S.fromList froms + + descs = S.unions (map (`descendents` po) froms) + + filtered = M.filterWithKey (\k _ -> not $ k `elem` froms) m + m' = + if S.null descs + then filtered + else M.insertWith S.union to descs filtered + + result = PartialOrder $ M.map go m' + + go s | hasFrom s = S.insert to $ S.union descs $ S.difference s from' + go s | otherwise = s + + hasFrom set = any (`S.member` set) froms diff --git a/src/Language/REST/Internal/Rewrite.hs b/src/Language/REST/Internal/Rewrite.hs new file mode 100644 --- /dev/null +++ b/src/Language/REST/Internal/Rewrite.hs @@ -0,0 +1,58 @@ +{-# 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 (Eq, Ord, Generic, Hashable, Show) + +type Subst = M.HashMap String RuntimeTerm + +getName :: Rewrite -> Maybe String +getName (Rewrite _t _u n) = n + +named :: Rewrite -> String -> Rewrite +named (Rewrite t u _) n = Rewrite t u (Just n) + +subst :: Subst -> MetaTerm -> RuntimeTerm +subst s (MT.Var v) | Just t <- M.lookup v s = t + | otherwise + = error $ printf "No value for metavar %s during subst %s" (show v) (show s) +subst s (MT.RWApp op xs) = App op (map (subst s) xs) + +unifyAll :: Subst -> [(MetaTerm, RuntimeTerm)] -> Maybe Subst +unifyAll su [] = Just su +unifyAll su ((x, y) : ts) + | Just s <- unify x y su + = unifyAll s ts + | otherwise + = Nothing + +unify :: MetaTerm -> RuntimeTerm -> Subst -> Maybe Subst +unify (MT.Var s) term su | M.lookup s su == Just term + = Just su +unify (MT.Var s) term su | M.lookup s su == Nothing + = Just $ M.insert s term su +unify (MT.RWApp o1 xs) (App o2 ys) su | o1 == o2 && length xs == length ys = + unifyAll su (zip xs ys) +unify _ _ _ = Nothing + +instance Monad m => RewriteRule m Rewrite RuntimeTerm where + apply t (Rewrite left right _) = return $ S.unions $ map go (subTerms t) + where + go (t', tf) | Just su <- unify left t' M.empty = S.singleton (tf $ subst su right) + go _ | otherwise = S.empty diff --git a/src/Language/REST/Internal/Util.hs b/src/Language/REST/Internal/Util.hs new file mode 100644 --- /dev/null +++ b/src/Language/REST/Internal/Util.hs @@ -0,0 +1,11 @@ +module Language.REST.Internal.Util where + +import qualified Data.List as L + +removeEqBy :: (Eq a) => (a -> a -> Bool) -> [a] -> [a] -> ([a], [a]) +removeEqBy _ [] ys = ([], ys) +removeEqBy f (x : xs) ys + | Just y <- L.find (f x) ys + = removeEqBy f xs $ L.delete y ys + | otherwise + = let (xs', ys') = removeEqBy f xs ys in (x : xs', ys') diff --git a/src/Language/REST/Internal/WQO.hs b/src/Language/REST/Internal/WQO.hs new file mode 100644 --- /dev/null +++ b/src/Language/REST/Internal/WQO.hs @@ -0,0 +1,336 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Language.REST.Internal.WQO ( + empty + , insert + , insertMaybe + , orderings + , getRelation + , merge + , mergeAll + , notStrongerThan + , WQO + , QORelation(..) + , ExtendOrderingResult(..) + , relevantTo + , singleton + , null + , getPO + , getECs + , elems) where + +import Prelude hiding (null, EQ, GT) +import GHC.Generics (Generic) +import qualified Data.Map as M +import Control.Monad +import Data.Hashable +import Data.Maybe +import qualified Data.List as L +import qualified Data.Set as S + +import qualified Language.REST.Internal.EquivalenceClass as EC +import qualified Language.REST.Internal.PartialOrder as PO +import Language.REST.Op +import Language.REST.SMT + +type PartialOrder = PO.PartialOrder +type EquivalenceClass = EC.EquivalenceClass + +data QORelation = QGT | QEQ deriving (Ord, Eq, Generic, Hashable) + +instance Show QORelation where + show QGT = ">" + show QEQ = "≈" + +instance {-# OVERLAPPING #-} ToSMTVar a Int => ToSMT (WQO a) Bool where + toSMT (WQO ecs po) = And $ ecsSMT ++ posSMT where + + toSMT' :: a -> SMTExpr Int + toSMT' = toSMT + + ecsSMT = do + ec <- S.toList ecs + let ecl = EC.toList ec + guard $ length ecl >= 2 + return $ Equal (map toSMT' ecl) + + posSMT = do + (ec, vs) <- PO.toDescsList po + var <- S.toList vs + return $ Greater (toSMT $ EC.head ec) (toSMT $ EC.head var) + + +getPO :: WQO a -> PartialOrder (EquivalenceClass a) +getPO (WQO _ po) = po + +getECs :: WQO a -> S.Set (EquivalenceClass a) +getECs (WQO ecs _) = ecs + +-- Invariant: the first set contains all ECs +data WQO a = WQO (S.Set (EquivalenceClass a)) (PartialOrder (EquivalenceClass a)) + deriving (Ord, Eq, Generic, Hashable) + +instance (Show a, Eq a, Hashable a) => Show (WQO a) where + show (WQO ecs _) | S.null ecs = "⊤" + show (WQO ecs po) = L.intercalate " ∧ " (map show ecs' ++ po') + where + ecs' = filter (not . EC.isSingleton) $ S.toList ecs + po' = + if PO.isEmpty po + then [] + else [show po] + -- else [show $ PO.mapUnsafe ecHead po] + -- ecHead (x, y) = (EC.head x, EC.head y) + +null :: Eq a => WQO a -> Bool +null wqo = wqo == empty + +empty :: WQO a +empty = WQO S.empty PO.empty + +singleton :: (Ord a, Eq a, Hashable a) => (a, a, QORelation) -> Maybe (WQO a) +singleton t = insertMaybe empty t + +{-# INLINE elems #-} +elems :: (Ord a) => WQO a -> S.Set a +elems (WQO ec _) = S.unions $ map EC.elems (S.toList ec) + +{-# INLINE getEquivalenceClasses #-} +getEquivalenceClasses :: (Ord a, Eq a, Hashable a) => WQO a -> a -> a + -> (Maybe (EquivalenceClass a), Maybe (EquivalenceClass a)) +getEquivalenceClasses (WQO classes _) source target = (t, u) + where + t = L.find (EC.isMember source) classes' + u = L.find (EC.isMember target) classes' + classes' = S.toList classes + +{-# INLINE getEquivalenceClasses' #-} +getEquivalenceClasses' + :: (Ord a, Hashable a) + => WQO a + -> a + -> a + -> Maybe (EC.EquivalenceClass a, EC.EquivalenceClass a) +getEquivalenceClasses' (WQO classes _) source target = + do + t <- L.find (EC.isMember source) classes' + if EC.isMember target t + then return (t, t) + else ((,) t) <$> L.find (EC.isMember target) classes' + where + classes' = S.toList classes + +{-# INLINE getRelation #-} +getRelation :: (Ord a, Eq a, Hashable a) => WQO a -> a -> a -> Maybe QORelation +getRelation _ f g | f == g = Just QEQ +getRelation wqo@(WQO _ po) source target + | Just (s, t) <- getEquivalenceClasses' wqo source target + = if s == t + then Just QEQ + else + if PO.gt po s t + then Just QGT + else Nothing + | otherwise = Nothing + +expandEC :: (Ord a, Eq a, Hashable a) => WQO a -> EquivalenceClass a -> a -> WQO a +expandEC (WQO ecs po) ec x = WQO ecs' po' + where + ec' = EC.insert x ec + ecs' = S.insert ec' $ S.delete ec ecs + po' = PO.replaceUnsafe [ec] ec' po + +mergeECs :: (Ord a, Eq a, Hashable a) => WQO a -> EquivalenceClass a -> EquivalenceClass a -> WQO a +mergeECs (WQO ecs po) ec1 ec2 = WQO ecs' po' + where + ec' = EC.union ec1 ec2 + ecs' = S.insert ec' $ S.delete ec2 $ S.delete ec1 ecs + po' = PO.replaceUnsafe [ec1, ec2] ec' po + +type ECMap a = M.Map (EquivalenceClass a) (EquivalenceClass a) + +{-# SPECIALISE notStrongerThan :: WQO Op -> WQO Op -> Bool #-} +notStrongerThan :: forall a . (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Bool +notStrongerThan w1 w2 | w1 == w2 = True +notStrongerThan (WQO ecs po) (WQO ecs' po') = result where + result = case mkEcsMap M.empty (S.toList ecs) of + Just ecsMap -> all (gt ecsMap) (PO.toDescsList po) + Nothing -> False + + mkEcsMap :: ECMap a -> [EquivalenceClass a] -> Maybe (ECMap a) + mkEcsMap buf [] = Just buf + mkEcsMap buf (ec:rest) = + do + ec' <- L.find (ec `EC.isSubsetOf`) (S.toList ecs') + mkEcsMap (M.insert ec ec' buf) rest + gt ecsMap (ec, descs) = + let + Just ec' = M.lookup ec ecsMap + in + descs `S.isSubsetOf` (PO.descendents ec' po') + + + + +mergeAll :: forall a. (Show a, Ord a, Eq a, Hashable a) => [WQO a] -> Maybe (WQO a) +mergeAll [] = Just empty +mergeAll [x] = Just x +mergeAll (x : x' : xs) = do + y <- merge x x' + mergeAll (y : xs) + +trace' :: String -> a -> a +trace' _ x = x + +{-# INLINE merge #-} +merge :: forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Maybe (WQO a) +merge lhs@(WQO ecs po) rhs@(WQO ecs' po') | S.disjoint (elems lhs) (elems rhs) + = Just $ WQO (S.union ecs ecs') (PO.unionDisjointUnsafe po po') +merge lhs rhs | otherwise = + if S.size (elems lhs) >= S.size (elems rhs) + then merge' lhs rhs + else merge' rhs lhs + +{-# SPECIALISE merge' :: WQO Op -> WQO Op -> Maybe (WQO Op) #-} +merge' :: forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Maybe (WQO a) +merge' lhs rhs@(WQO ecs po) = trace' message $ result where + + message = "Merge " ++ (show $ hash lhs) ++ " " ++ (show $ hash rhs) + + withEQs' = go lhs ecsFacts + + result = do + withEQs <- withEQs' + go withEQs poFacts + + ecsFacts :: [(a, a, QORelation)] + ecsFacts = concatMap ecFacts (S.toList ecs) + + ecFacts ec = + let + xs = EC.toList ec + in + map (\(a, b) -> (a, b, QEQ)) (zip xs (tail xs)) + + poFacts :: [(a, a, QORelation)] + poFacts = + map (\(a, b) -> (head (EC.toList a), head (EC.toList b), QGT)) (PO.toList po) + + go r [] = Just r + go r (x : xs) = + do + r' <- insertMaybe r x + go r' xs + + +data ExtendOrderingResult a = + ValidExtension (WQO a) + | AlreadyImplied + | Contradicts + +relevantTo :: (Ord a, Eq a, Hashable a) => WQO a -> S.Set a -> S.Set a -> WQO a +relevantTo wqo0 as bs = go empty cartesianProduct where + + cartesianProduct = do + x <- S.toList as + y <- S.toList bs + return (x, y) + + get _ (ValidExtension w) = w + get w AlreadyImplied = w + get _ _ = undefined + + go wqo [] = wqo + go wqo ((f, g) : xs) | f == g = go wqo xs + go wqo ((f, g) : xs) | Just r <- getRelation wqo0 f g + , wqo' <- get wqo $ insert wqo (f, g, r) + = go wqo' xs + go wqo ((f, g) : xs) | Just r <- getRelation wqo0 g f + , wqo' <- get wqo $ insert wqo (g, f, r) + = go wqo' xs + go wqo (_ : xs) | otherwise = go wqo xs + +{-# INLINE insertMaybe #-} +{-# SPECIALISE insertMaybe :: WQO Op -> (Op, Op, QORelation) -> Maybe (WQO Op) #-} +insertMaybe :: (Ord a, Eq a, Hashable a) => WQO a -> (a, a, QORelation) -> Maybe (WQO a) +insertMaybe wqo t = case insert wqo t of + ValidExtension wqo' -> Just wqo' + AlreadyImplied -> Just wqo + Contradicts -> Nothing + + + +{-# SPECIALISE insert :: WQO Op -> (Op, Op, QORelation) -> ExtendOrderingResult Op #-} +insert :: (Ord a, Eq a, Hashable a) => WQO a -> (a, a, QORelation) -> ExtendOrderingResult a +insert _ (f, g, QGT) | f == g = Contradicts +insert wqo (f, g, r) | Just r' <- getRelation wqo f g + = if r == r' then AlreadyImplied else Contradicts +insert wqo (f, g, _) | isJust $ getRelation wqo g f = Contradicts + +insert wqo@(WQO ecs po) (f, g, QEQ) = ValidExtension $ + case getEquivalenceClasses wqo f g of + (Nothing, Nothing) -> + let + ecs' = S.insert (EC.fromList [f, g]) ecs + in + WQO ecs' po + (Just ec, Nothing) -> expandEC wqo ec g + (Nothing, Just ec) -> expandEC wqo ec f + (Just ec1, Just ec2) -> mergeECs wqo ec1 ec2 + +insert wqo@(WQO ecs po) (f, g, QGT) = ValidExtension $ + case getEquivalenceClasses wqo f g of + (Nothing, Nothing) -> + let + f' = EC.singleton f + g' = EC.singleton g + ecs' = S.insert f' $ S.insert g' ecs + Just po' = PO.insert po f' g' + in + WQO ecs' po' + (Just ec, Nothing) -> + let + g' = EC.singleton g + ecs' = S.insert g' ecs + Just po' = PO.insert po ec g' + in + WQO ecs' po' + + (Nothing, Just ec) -> + let + f' = EC.singleton f + ecs' = S.insert f' ecs + Just po' = PO.insert po f' ec + in + WQO ecs' po' + (Just ec1, Just ec2) -> + WQO ecs (PO.insertUnsafe po ec1 ec2) + + +orderings :: forall a. (Ord a, Eq a, Hashable a) => S.Set a -> S.Set (WQO a) +orderings ops = go S.empty (S.singleton empty) where + + insert' w t | ValidExtension w' <- insert w t = Just w' + insert' _ _ = Nothing + + go :: S.Set (WQO a) -> S.Set (WQO a) -> S.Set (WQO a) + go seen acc | S.null acc = seen + go seen acc = + let + ordering = head $ S.toList acc + acc' = S.delete ordering acc + seen' = S.insert ordering seen + newOrderings = + S.fromList $ do + f <- S.toList ops + g <- S.toList (S.delete f ops) + o <- [QEQ, QGT] + maybeToList (insert' ordering (f,g, o)) + newOrderings' = S.difference newOrderings seen + in + go seen' (S.union acc' newOrderings') diff --git a/src/Language/REST/Internal/WorkStrategy.hs b/src/Language/REST/Internal/WorkStrategy.hs new file mode 100644 --- /dev/null +++ b/src/Language/REST/Internal/WorkStrategy.hs @@ -0,0 +1,39 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Language.REST.Internal.WorkStrategy where + +import Language.REST.ExploredTerms as ET +import Language.REST.Path +import Language.REST.Internal.Rewrite + +import Data.Hashable +import qualified Data.List as L + +type GetWork m rule term et oc = [Path rule term oc] -> (term -> et) -> ExploredTerms et oc m -> (Path rule term oc, [Path rule term oc]) + +newtype WorkStrategy rule term et oc = WorkStrategy (forall m . GetWork m rule term et oc) + +bfs :: WorkStrategy rule term et oc +bfs = WorkStrategy bfs' + +notVisitedFirst :: (Eq term, Eq rule, Eq oc, Eq et, Hashable et) => WorkStrategy rule term et oc +notVisitedFirst = WorkStrategy notVisitedFirst' + +bfs' :: [Path rule term oc] -> (term -> et) -> ExploredTerms et oc m -> (Path rule term oc, [Path rule term oc]) +bfs' (h:t) _ _ = (h, t) +bfs' _ _ _ = error "empty path list" + +notVisitedFirst' :: (Eq term, Eq rule, Eq oc, Eq et, Hashable et) => GetWork m rule term et oc +notVisitedFirst' paths toET et = + case L.find (\p -> not (ET.visited (toET $ runtimeTerm p) et)) paths of + Just p -> (p, L.delete p paths) + Nothing -> (head paths, tail paths) + +commutesLast :: forall term oc et . (Eq term, Eq oc, Eq et, Hashable et) => WorkStrategy Rewrite term et oc +commutesLast = WorkStrategy go where + go paths toET et = + case L.find (\p -> not (ET.visited (toET $ runtimeTerm p) et || fromComm p)) paths of + Just p -> (p, L.delete p paths) + Nothing -> (head paths, tail paths) + fromComm ([], _) = False + fromComm (steps, _) = (getName . rule . last) steps == Just "mpComm" diff --git a/src/Language/REST/KBO.hs b/src/Language/REST/KBO.hs new file mode 100644 --- /dev/null +++ b/src/Language/REST/KBO.hs @@ -0,0 +1,46 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NamedFieldPuns #-} + +module Language.REST.KBO (kbo, kboGTE) where + +import Language.REST.OCAlgebra +import Language.REST.Op +import Language.REST.RuntimeTerm as RT +import Language.REST.SMT +import Language.REST.Internal.Util + +import qualified Data.Map as M + +termOps :: RuntimeTerm -> [Op] +termOps (App f xs) = f:(concatMap termOps xs) + +arityConstraints :: RuntimeTerm -> SMTExpr Bool +arityConstraints t = toExpr $ go M.empty t where + go :: M.Map Op Int -> RuntimeTerm -> M.Map Op Int + go m (App f []) = M.insert f 1 m + go m (App f [targ]) = go (M.insert f 1 m) targ + go m (App f ts) = foldl go (M.insert f 0 m) ts + + toExpr m = And $ map toConstraint (M.toList m) + toConstraint (sym, n) = toSMT sym `smtGTE` (Const n) + + +kboGTE :: RuntimeTerm -> RuntimeTerm -> SMTExpr Bool +kboGTE t u = arityConstraints t `smtAnd` arityConstraints u `smtAnd` (size tOps `smtGTE` size uOps) + where + (tOps, uOps) = removeEqBy (==) (termOps t) (termOps u) + size ops = smtAdd (map toSMT ops) + + +kbo :: SolverHandle -> OCAlgebra (SMTExpr Bool) RuntimeTerm IO +kbo solver = OCAlgebra + { isSat = checkSat' solver + , refine + , top = smtTrue + , union + , notStrongerThan + } + where + union e1 e2 = Or [e1, e2] + refine e t u = e `smtAnd` kboGTE t u + notStrongerThan e1 e2 = checkSat' solver (Implies e2 e1) diff --git a/src/Language/REST/LPO.hs b/src/Language/REST/LPO.hs new file mode 100644 --- /dev/null +++ b/src/Language/REST/LPO.hs @@ -0,0 +1,89 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ImplicitParams #-} + +module Language.REST.LPO (lpo, lpoStrict) where + +import Prelude hiding (EQ, GT, lex) + +import Control.Monad.Identity +import Data.Hashable + +import Language.REST.Op +import Language.REST.Internal.OpOrdering as OpOrdering +import Language.REST.WQOConstraints as OC +import Language.REST.Types +import Language.REST.RuntimeTerm + +lex + :: (Eq a, Ord b, Hashable b) + => WQOConstraints impl m + -> Bool + -> impl b + -> (WQOConstraints impl m -> Relation -> impl b -> a -> a -> impl b) + -> [a] + -> [a] + -> impl b +lex oc strict cs f (t:ts) (u:us) | t == u = lex oc strict cs f ts us +lex oc strict cs f (t:ts) (u:us) = union oc case1 case2 + where + -- t > u + case1 = f oc GT cs t u + -- t = u + case2 = + let + cs' = f oc EQ cs t u + in + lex oc strict cs' f ts us +lex oc _ _ _ [] (_:_) = unsatisfiable oc +lex _ _ cs _ (_:_) [] = cs +lex oc strict cs _ [] [] = if strict then unsatisfiable oc else cs + +lpo' :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => + Bool -> WQOConstraints oc m -> Relation -> oc Op -> RuntimeTerm -> RuntimeTerm -> oc Op +-- lpo' False oc EQ cs t u = intersect oc (lpo' False oc GTE cs t u) (lpo' False oc GTE cs u t) +lpo' False oc EQ _cs (App _f ts) (App _g us) | length ts /= length us = unsatisfiable oc +lpo' False oc EQ cs (App f ts) (App g us) = + let + cs' = intersect oc cs (singleton oc $ f =. g) + subs = map (uncurry $ lpo' False oc EQ cs') (zip ts us) + in + intersectAll oc (cs' : subs) + +lpo' True oc EQ cs t u = if t == u then cs else unsatisfiable oc +lpo' strict oc r cs t@(App f ts) u@(App g us) = result + where + result = intersect oc cs result' + result' = unionAll oc [case1, case2, case3] + + -- tᵢ ≥ u for some i + case1 = unionAll oc (map go ts) where + go ti = lpo' strict oc GTE cs ti u + + -- f > g ∧ t > uⱼ for all j + case2 = + if f == g + then unsatisfiable oc + else intersect oc tDominatesUs (singleton oc $ f >. g) + + -- f = g ∧ t > uⱼ for all j ts >lex us + case3 = + if strict && f /= g + then unsatisfiable oc + else intersectAll oc ([tDominatesUs, (lex oc (r == GT) cs (lpo' strict) ts us)] ++ symEQ) where + symEQ = if f == g then [] else [singleton oc (f =. g)] + + + tDominatesUs = intersectAll oc (map go us) where + go ui = lpo' strict oc GT cs t ui + + +lpo :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RuntimeTerm Identity +lpo oc r cs t u = return $ lpo' False oc r cs t u + +lpoStrict :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RuntimeTerm Identity +lpoStrict oc r cs t u = return $ lpo' True oc r cs t u diff --git a/src/Language/REST/MultiSet.hs b/src/Language/REST/MultiSet.hs deleted file mode 100644 --- a/src/Language/REST/MultiSet.hs +++ /dev/null @@ -1,80 +0,0 @@ -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveAnyClass #-} - -module Language.REST.MultiSet - ( MultiSet - , delete - , deleteMany - , distinctElems - , empty - , filter - , insert - , member - , null - , toList - , toOccurList - , singleton - , fromList - , toSet - ) where - -import Prelude hiding (null, filter, delete) - -import GHC.Generics -import Data.Hashable -import qualified Data.List as L -import qualified Data.HashMap.Strict as M -import qualified Data.HashSet as S - -data MultiSet a = MultiSet (M.HashMap a Int) deriving (Eq, Generic, Hashable, Ord) - -instance Show a => Show (MultiSet a) where - show ms = "{" ++ L.intercalate ", " (map show $ toList ms) ++ "}" - -delete :: (Hashable a, Eq a) => a -> MultiSet a -> MultiSet a -delete k = deleteMany k 1 - -deleteMany :: (Hashable a, Eq a) => a -> Int -> MultiSet a -> MultiSet a -deleteMany k v (MultiSet ms) | Just c <- M.lookup k ms - , c > v = MultiSet $ M.insert k (c - v) ms -deleteMany k _ (MultiSet ms) | otherwise = MultiSet $ M.delete k ms - -distinctElems :: MultiSet a -> [a] -distinctElems (MultiSet ms) = M.keys ms - -empty :: MultiSet a -empty = MultiSet M.empty - -toOccurList :: MultiSet a -> [(a, Int)] -toOccurList (MultiSet ms) = M.toList ms - -filter :: (a -> Bool) -> MultiSet a -> MultiSet a -filter f (MultiSet ms) = MultiSet $ M.filterWithKey f' ms - where - f' k _ = f k - -null :: MultiSet a -> Bool -null (MultiSet ms) = M.null ms - -member :: (Eq a, Hashable a) => a -> MultiSet a -> Bool -member k (MultiSet ms) = M.member k ms - -toList :: MultiSet a -> [a] -toList ms = concatMap go (toOccurList ms) - where - go (k, num) = take num $ repeat k - -insert :: (Eq a, Hashable a) => a -> MultiSet a -> MultiSet a -insert k (MultiSet ms) | Just c <- M.lookup k ms - = MultiSet $ M.insert k (c + 1) ms -insert k (MultiSet ms) | otherwise - = MultiSet $ M.insert k 1 ms - -singleton :: (Eq a, Hashable a) => a -> MultiSet a -singleton k = MultiSet (M.singleton k 1) - -fromList :: (Eq a, Hashable a) => [a] -> MultiSet a -fromList = foldl (flip insert) empty - -toSet :: MultiSet a -> S.HashSet a -toSet (MultiSet ms) = M.keysSet ms diff --git a/src/Language/REST/MultisetOrder.hs b/src/Language/REST/MultisetOrder.hs deleted file mode 100644 --- a/src/Language/REST/MultisetOrder.hs +++ /dev/null @@ -1,79 +0,0 @@ -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveAnyClass #-} - -module Language.REST.MultisetOrder (multisetOrder, possibilities) where - -import GHC.Generics -import qualified Data.List as L -import Debug.Trace (trace) -import Prelude hiding (EQ, GT) -import Data.Hashable -import qualified Data.HashSet as S -import Text.Printf - -import qualified Language.REST.MultiSet as M -import Language.REST.OrderingConstraints as OC -import Language.REST.Types - -type MultiSet = M.MultiSet - -trace' :: String -> a -> a --- trace' = trace -trace' _ x = x - -removeEQs :: (Eq x, Ord x, Hashable x) => MultiSet x -> MultiSet x -> (MultiSet x, MultiSet x) -removeEQs ts0 us0 = go (M.toList ts0) M.empty us0 where - go [] ts us = (ts, us) - go (x : xs) ts us | x `M.member` us = go xs ts (M.delete x us) - go (x : xs) ts us | otherwise = go xs (M.insert x ts) us - -data Replace a = - ReplaceOne a a - | Replace a (S.HashSet a) - deriving (Eq, Hashable, Generic, Show) - -powerset [] = [[]] -powerset (x:xs) = [x:ps | ps <- powerset xs] ++ powerset xs - -possibilities :: (Hashable a, Eq a) => Relation -> [a] -> [a] -> S.HashSet (S.HashSet (Replace a)) -possibilities r [] [] = if r == GT then S.empty else S.singleton (S.empty) -possibilities r xs [] = if r == EQ then S.empty else S.singleton (S.fromList $ map (flip Replace S.empty) xs) -possibilities _ [] (_:_) = S.empty -possibilities r (x:xs) ys = if r == EQ then eqs else S.union eqs doms where - eqs = S.unions $ map go ys where - go y = S.map (S.insert (ReplaceOne x y)) (possibilities r xs (L.delete y ys)) - doms = S.unions $ map go (powerset $ L.nub ys) where - go ys' = S.map - (S.insert (Replace x (S.fromList ys'))) - (possibilities GTE xs (filter (not . flip elem ys') ys)) - - -multisetOrder :: forall oc base lifted m . (Ord lifted, Ord base, Show base, Eq base, Hashable base, Hashable lifted, Eq lifted, Show (oc base), Eq (oc base), Monad m) => - ConstraintGen oc base lifted m - -> ConstraintGen oc base (MultiSet lifted) m -multisetOrder _ impl _ oc _ _ | oc == unsatisfiable impl = return $ unsatisfiable impl -multisetOrder underlying impl r oc ts0 us0 = (uncurry go) (removeEQs ts0 us0) where - go :: MultiSet lifted -> MultiSet lifted -> m (oc base) - go ts us | M.null ts && M.null us = return $ if r == GT then unsatisfiable impl else oc - go ts us | not (M.null ts) && M.null us = return $ if r == EQ then unsatisfiable impl else oc - go ts us | M.null ts && not (M.null us) = return $ unsatisfiable impl - go ts us = result - where - - pos = possibilities r (M.toList ts) (M.toList us) - - result = - trace' ("There are " ++ (show $ S.size pos) ++ " possibilities") $ - unionAll impl <$> mapM posConstraints (S.toList pos) - - posConstraints pos1 = L.foldl' apply (return oc) (S.toList pos1) where - apply moc (ReplaceOne t u) = do - oc' <- moc - underlying impl EQ oc' t u - apply moc (Replace t ts') = do - oc' <- moc - if S.null ts' - then return oc' - else intersectAll impl <$> (mapM (underlying impl GT oc' t) (S.toList ts')) diff --git a/src/Language/REST/OCAlgebra.hs b/src/Language/REST/OCAlgebra.hs new file mode 100644 --- /dev/null +++ b/src/Language/REST/OCAlgebra.hs @@ -0,0 +1,51 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Language.REST.OCAlgebra where + +data OCAlgebra c a m = OCAlgebra + { + isSat :: c -> m Bool + , refine :: c -> a -> a -> c + , top :: c + + -- For explore optimizations, if not required just make it return 2nd param + , union :: c -> c -> c + -- If not required return False + , notStrongerThan :: c -> c -> m Bool + } + +fuelOC :: (Monad m) => Int -> OCAlgebra Int a m +fuelOC initFuel = OCAlgebra isSat' refine' initFuel union' notStrongerThan' + where + isSat' c = return $ c >= 0 + refine' c _ _ = c - 1 + union' c c' = max c c' + notStrongerThan' c c' = return $ c >= c' + +contramap :: forall c a b m . + (b -> a) + -> OCAlgebra c a m + -> OCAlgebra c b m +contramap f aoc = aoc{refine = refine'} + where + refine' :: c -> b -> b -> c + refine' c t1 t2 = refine aoc c (f t1) (f t2) + +bimapConstraints :: forall c d a m . + (c -> d) + -> (d -> c) + -> OCAlgebra c a m + -> OCAlgebra d a m +bimapConstraints to from aoc = OCAlgebra isSat' refine' (to (top aoc)) union' notStrongerThan' + where + isSat' :: d -> m Bool + isSat' c = isSat aoc (from c) + + refine' :: d -> a -> a -> d + refine' c t1 t2 = to $ refine aoc (from c) t1 t2 + + union' :: d -> d -> d + union' c1 c2 = to $ union aoc (from c1) (from c2) + + notStrongerThan' :: d -> d -> m Bool + notStrongerThan' c1 c2 = notStrongerThan aoc (from c1) (from c2) diff --git a/src/Language/REST/OCToAbstract.hs b/src/Language/REST/OCToAbstract.hs --- a/src/Language/REST/OCToAbstract.hs +++ b/src/Language/REST/OCToAbstract.hs @@ -7,24 +7,23 @@ module Language.REST.OCToAbstract where import Data.Hashable -import Debug.Trace import Control.Monad.Identity -import Language.REST.AbstractOC -import qualified Language.REST.OrderingConstraints as OC +import Language.REST.OCAlgebra +import qualified Language.REST.WQOConstraints as OC import Language.REST.Types -import Language.REST.SMT +import Language.REST.SMT (ToSMTVar) showHash :: Show a => a -> String showHash = show . hash . show lift :: forall impl base lifted m . (ToSMTVar base Int, Ord base, Eq base, Hashable base, Show lifted, Show base, Show (impl base)) => - OC.OrderingConstraints impl m + OC.WQOConstraints impl m -> OC.ConstraintGen impl base lifted Identity - -> AbstractOC (impl base) lifted m + -> OCAlgebra (impl base) lifted m lift oc cgen = - AbstractOC { + OCAlgebra { isSat = isSat' , top = top' , refine = refine' @@ -41,13 +40,7 @@ refine' :: impl base -> lifted -> lifted -> impl base refine' c t u = let - msg = "Start refine " ++ (show t) ++ " >= " ++ (show u) ++ " from " ++ show c ++ "\n\n\n" - pair = -- trace' msg $ - runIdentity $ cgen oc GTE top' t u - result = -- trace' ("Start intersect " ++ showHash pair ++ "\n\n\n with \n\n" ++ showHash c) $ - OC.intersect oc c pair + pair = runIdentity $ cgen oc GTE top' t u + result = OC.intersect oc c pair in result - --- trace' _ x = x -trace' = trace diff --git a/src/Language/REST/Op.hs b/src/Language/REST/Op.hs --- a/src/Language/REST/Op.hs +++ b/src/Language/REST/Op.hs @@ -9,7 +9,6 @@ import Data.Hashable import Data.String import GHC.Generics (Generic) -import Data.Text import Language.REST.SMT newtype Op = Op Text deriving (Eq, Ord, Hashable, Generic) diff --git a/src/Language/REST/OpOrdering.hs b/src/Language/REST/OpOrdering.hs deleted file mode 100644 --- a/src/Language/REST/OpOrdering.hs +++ /dev/null @@ -1,104 +0,0 @@ -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE TypeSynonymInstances #-} - - -module Language.REST.OpOrdering ( - empty - , merge - , OpOrdering - , opInsert - , opGT - , opEQ - , (=.) - , (>.) - , parseOO - ) where - -import Prelude hiding (GT, EQ) -import GHC.Generics (Generic) -import Data.Hashable -import Data.Maybe -import qualified Data.Text as T -import qualified Data.HashSet as S -import Text.ParserCombinators.Parsec.Char -import Text.ParserCombinators.Parsec -import Text.Parsec (parserTrace) - -import qualified Language.REST.PartialOrder as PO -import Language.REST.Op -import Language.REST.Types -import Language.REST.WQO as WQO - - -type PartialOrder = PO.PartialOrder -type OpOrdering = WQO Op - - -opGT :: OpOrdering -> Op -> Op -> Bool -opGT s f g = getRelation s f g == Just QGT - -opEQ :: OpOrdering -> Op -> Op -> Bool -opEQ s f g = getRelation s f g == Just QEQ - - -opInsert :: OpOrdering -> Op -> Op -> QORelation -> Maybe OpOrdering -opInsert o f g r = - case WQO.insert o (f, g, r) of - ValidExtension o' -> Just o' - _ -> Nothing - --- The following only are valid if f /= g. - --- precondition : f /= g -(>.) :: Op -> Op -> OpOrdering -(>.) f g = fromJust $ WQO.singleton (f, g, QGT) - --- precondition : f /= g -(=.) :: Op -> Op -> OpOrdering -(=.) f g = fromJust $ WQO.singleton (f, g, QEQ) - --- precondition : f /= g -(<.) :: Op -> Op -> OpOrdering -(<.) f g = g >. f - -parseOO :: String -> Maybe OpOrdering -parseOO str = - case parse parser "" str of - Left err -> error (show err) - Right t -> t - -parser = fmap mergeAll' (sepBy1 atom conj) where - - mergeAll' :: [Maybe OpOrdering] -> Maybe OpOrdering - mergeAll' [x] = x - mergeAll' (Just x : Just x' : xs) = - do - x'' <- merge x x' - mergeAll' (Just x'' : xs) - mergeAll' _ = Nothing - - conj = spaces >> (char '\8743' <|> char '^') >> spaces - eq = spaces >> char '=' >> spaces - gt = spaces >> char '>' >> spaces - - - atom = try gtAtom <|> try eqAtom - - eqAtom = fmap allEQ (sepBy1 sym (try eq)) - where - mkEQ f g = WQO.singleton (f, g, QEQ) - allEQ syms = - let - pairs = zipWith mkEQ syms (tail syms) - in - mergeAll' pairs - - gtAtom = do - left <- sym - _ <- gt - right <- sym - return $ WQO.singleton (left, right, QGT) - - sym = fmap (Op . T.pack) (many (alphaNum <|> char '+' <|> char '*')) diff --git a/src/Language/REST/OrderingConstraints.hs b/src/Language/REST/OrderingConstraints.hs deleted file mode 100644 --- a/src/Language/REST/OrderingConstraints.hs +++ /dev/null @@ -1,113 +0,0 @@ -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE FlexibleContexts #-} -module Language.REST.OrderingConstraints - ( - OrderingConstraints(..) - , ConstraintGen - , liftC - , cmapConstraints - , numOrderings - , isUnsatisfiable - , intersectAll - , unionAll - , intersectRelation - , runStateConstraints - , singleton - , simplify - ) where - -import Control.Monad.Identity -import Control.Monad.State.Strict -import qualified Data.List as L -import Data.Hashable -import Debug.Trace -import qualified Data.Set as S - -import Prelude hiding (GT, EQ) - -import qualified Language.REST.WQO as WQO -import Language.REST.Types -import Language.REST.SMT - -type WQO = WQO.WQO - -trace' _ x = x - -data OrderingConstraints impl m = OC - { addConstraint :: forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a - , intersect :: forall a. (Show a, Eq a, Ord a, Hashable a) => impl a -> impl a -> impl a - , isSatisfiable :: forall a. (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => impl a -> m Bool - , notStrongerThan :: forall a. (ToSMTVar a Int, Eq a, Ord a, Hashable a) => impl a -> impl a -> m Bool - , noConstraints :: forall a. (Eq a, Ord a, Hashable a) => impl a - , permits :: forall a. (Show a, Eq a, Ord a, Hashable a) => impl a -> WQO a -> Bool - , relevantConstraints :: forall a. (Eq a, Ord a, Hashable a) => impl a -> S.Set a -> S.Set a -> impl a - , union :: forall a. (Eq a, Ord a, Hashable a) => impl a -> impl a -> impl a - , unsatisfiable :: forall a. impl a - , elems :: forall a. (Eq a, Ord a, Hashable a) => impl a -> S.Set a - , getOrdering :: forall a. impl a -> Maybe (WQO a) - , simplify :: forall a. (Eq a, Ord a, Hashable a) => impl a -> impl a - } - -numOrderings :: (Show a, Ord a, Eq a, Ord a, Hashable a) => S.Set a -> OrderingConstraints oc m -> oc a -> Int -numOrderings elems impl oc = S.size $ S.filter (permits impl oc) (WQO.orderings elems) - -isUnsatisfiable :: (Functor m, ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => OrderingConstraints oc m -> oc a -> m Bool -isUnsatisfiable OC{isSatisfiable} c = not <$> isSatisfiable c - -singleton :: (Eq a, Ord a, Hashable a) => OrderingConstraints oc m -> WQO a -> oc a -singleton OC{addConstraint, noConstraints} c = addConstraint c noConstraints - -intersectAll :: (Eq a, Ord a, Hashable a, Show a, Show (oc a)) => OrderingConstraints oc m -> [oc a] -> oc a -intersectAll OC{noConstraints} [] = noConstraints -intersectAll OC{intersect} (x:xs) = L.foldl' go x xs - where - go t1 t2 = trace' ("Intersect " ++ (show t1)) $ intersect t1 t2 - -unionAll :: (Eq a, Ord a, Hashable a, Show a, Show (oc a)) => OrderingConstraints oc m -> [oc a] -> oc a -unionAll OC{unsatisfiable} [] = unsatisfiable -unionAll OC{union} (x:xs) = L.foldl' go x xs - where - go t1 t2 = trace' ("Union " ++ (show t1)) $ union t1 t2 - -intersectRelation :: - (Ord a, Eq a, Ord a, Hashable a, Show a) => - OrderingConstraints oc m -> oc a -> (a, a, Relation) -> oc a -intersectRelation oc impl (f, g, r) = - case nc r of - Just impl' -> intersect oc impl impl' - Nothing -> unsatisfiable oc - where - nc GT = fmap (singleton oc) (WQO.singleton (f, g, WQO.QGT)) - nc EQ = fmap (singleton oc) (WQO.singleton (f, g, WQO.QEQ)) - nc GTE = do - wqo1 <- WQO.singleton (f, g, WQO.QGT) - wqo2 <- WQO.singleton (f, g, WQO.QEQ) - return $ union oc (singleton oc wqo1) (singleton oc wqo2) - - - --- ConstraintGen impl R >= t u returns the constraints on >= that guarantee --- the resulting relation >=', we have: --- 1. x >= y implies x >=' y --- 2. t lift(R(>=')) u --- Where R generates { == , >=, > } from the underlying ordering --- R is used to enable optimizations - -type ConstraintGen oc base lifted m = - forall m' . (OrderingConstraints oc m' -> Relation -> oc base -> lifted -> lifted -> m (oc base)) - -cmapConstraints :: (lifted' -> lifted) -> ConstraintGen oc base lifted m -> ConstraintGen oc base lifted' m -cmapConstraints f cgen impl r oc t u = cgen impl r oc (f t) (f u) - -liftC :: (m Bool -> m' Bool) -> OrderingConstraints impl m -> OrderingConstraints impl m' -liftC f oc = oc{ - isSatisfiable = isSatisfiable' - , notStrongerThan = notStrongerThan' - } - where - isSatisfiable' c1 = f (isSatisfiable oc c1) - notStrongerThan' c1 c2 = f (notStrongerThan oc c1 c2) - -runStateConstraints :: ConstraintGen oc base lifted (State a) -> a -> ConstraintGen oc base lifted Identity -runStateConstraints cgen initState impl r oc t u = Identity $ evalState (cgen impl r oc t u) initState diff --git a/src/Language/REST/OrderingConstraints/ADT.hs b/src/Language/REST/OrderingConstraints/ADT.hs deleted file mode 100644 --- a/src/Language/REST/OrderingConstraints/ADT.hs +++ /dev/null @@ -1,244 +0,0 @@ -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE CPP #-} - -#define OPTIMIZE_WQO - -module Language.REST.OrderingConstraints.ADT where - -import GHC.Generics (Generic) - -import Debug.Trace -import Data.Hashable -import Control.Monad.State.Lazy -import qualified Data.Set as S -import qualified Data.Maybe as Mb -import qualified Data.Map.Strict as M -import qualified Language.REST.WQO as WQO -import qualified Language.REST.OrderingConstraints as OC -import Language.REST.SMT -import Language.REST.Op -import System.IO.Unsafe -import Text.Printf - -type WQO = WQO.WQO - -data ConstraintsADT a = - Sat (WQO a) - | Unsat - | Union (ConstraintsADT a) (ConstraintsADT a) - | Intersect (ConstraintsADT a) (ConstraintsADT a) - deriving (Eq, Ord, Generic, Hashable) - -instance {-# OVERLAPPING #-} (ToSMTVar a Int) => ToSMT (ConstraintsADT a) Bool where - toSMT (Sat w) = toSMT w - toSMT Unsat = smtFalse - toSMT (Union w1 w2) = Or [toSMT w1, toSMT w2] - toSMT (Intersect w1 w2) = And [toSMT w1, toSMT w2] - -{-# SPECIALIZE cost :: ConstraintsADT Op -> Int #-} -cost :: (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int -cost (Union lhs rhs) = min (cost lhs) (cost rhs) -cost (Intersect lhs rhs) = cost lhs + cost rhs -cost (Sat wqo) = S.size $ WQO.elems wqo -cost Unsat = 100 - -minDepth :: ConstraintsADT a -> Int -minDepth (Union lhs rhs) = 1 + min (minDepth lhs) (minDepth rhs) -minDepth (Intersect lhs rhs) = 1 + min (minDepth lhs) (minDepth rhs) -minDepth _ = 1 - -maxDepth :: ConstraintsADT a -> Int -maxDepth (Union lhs rhs) = 1 + max (maxDepth lhs) (maxDepth rhs) -maxDepth (Intersect lhs rhs) = 1 + max (maxDepth lhs) (maxDepth rhs) -maxDepth _ = 1 - -intersect :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a - -#ifdef OPTIMIZE_WQO --- Optimization -intersect (Sat t) (Sat u) = - case WQO.merge t u of - Just t' -> Sat t' - Nothing -> Unsat -#endif - -intersect (Sat w) v | w == WQO.empty = v -intersect v (Sat w) | w == WQO.empty = v -intersect _ Unsat = Unsat -intersect Unsat _ = Unsat -intersect t1 t2 | t1 == t2 = t1 -intersect t1 (Union t2 t3) | t1 == t2 || t1 == t3 = t1 -#ifdef OPTIMIZE_WQO -intersect (Sat w1) (Intersect (Sat w2) t2) = - case WQO.merge w1 w2 of - Just w' -> intersect (Sat w') t2 - Nothing -> Unsat -intersect (Sat w1) (Intersect t2 (Sat w2)) = - case WQO.merge w1 w2 of - Just w' -> intersect (Sat w') t2 - Nothing -> Unsat -intersect (Intersect t1 (Sat w1)) (Sat w2) = - case WQO.merge w1 w2 of - Just w' -> intersect t1 (Sat w') - Nothing -> Unsat -intersect (Intersect (Sat w1) t1) (Sat w2) = - case WQO.merge w1 w2 of - Just w' -> intersect t1 (Sat w') - Nothing -> Unsat -#endif -intersect t1 t2 = Intersect t1 t2 - -union (Sat w) _ | w == WQO.empty = Sat w -union _ (Sat w) | w == WQO.empty = Sat w -union (Intersect a b) c | a == c || b == c = c -union a (Intersect b c) | a == b || a == c = a -union a (Union b c) | a == b = union a c -union Unsat s = s -union s Unsat = s -union c1 c2 | c1 == c2 = c1 -union c1 c2 = Union c1 c2 - -addConstraint o c = intersect (Sat o) c - -relevantConstraints c _ _ = c - -notStrongerThan t1 t2 | t1 == t2 = smtTrue -notStrongerThan t1 _ | t1 == noConstraints = smtTrue -notStrongerThan t1 t2 | otherwise = Implies (toSMT t2) (toSMT t1) - -noConstraints = Sat (WQO.empty) -unsatisfiable = Unsat - -trace' = trace - -{-# SPECIALIZE getConstraints :: ConstraintsADT Op -> [WQO Op] #-} -getConstraints :: forall a. (Show a, Ord a, Hashable a) => ConstraintsADT a -> [WQO a] -getConstraints adt = -- trace' ("Get constraints, size : " ++ (show $ dnfSize adt)) $ - evalState (getConstraints' adt) (GCState M.empty M.empty) - -data GCState a = GCState { - cs :: M.Map (ConstraintsADT a) (GCResult a) - , ms :: M.Map (WQO a, WQO a) (Maybe (WQO a)) -} - -type GCResult a = [WQO a] - -type GCMonad a = State (GCState a) (GCResult a) - -cached :: (Ord a) => ConstraintsADT a -> GCMonad a -> GCMonad a -cached key thunk = do - cache <- gets cs - case M.lookup key cache of - Just result -> trace' ("ADT Cache hit") $ return result - Nothing -> trace' ("ADT Cache miss") $ do - result <- trace' "Do thunk" thunk - trace' "Done" $ modify (\st -> st{cs = M.insert key result (cs st)}) - return result - where - trace' _ x = x - -- trace' = trace - -cached' :: (Hashable a, Show a, Ord a) => (WQO a, WQO a) -> Maybe (WQO a) -> State (GCState a) (Maybe (WQO a)) -cached' (lhs, rhs) thunk = do - cache <- gets ms - case M.lookup (lhs, rhs) cache of - Just result -> trace' ("WQO Cache hit") $ return result - Nothing -> trace' ("WQO Cache miss" ++ show (lhs, rhs)) $ do - trace' "Done" $ modify (\st -> st{ms = M.insert (rhs, lhs) thunk $ M.insert (lhs, rhs) thunk (ms st)}) - return thunk - where - trace' _ x = x - -- trace' = trace - -getConstraints' :: forall a. (Show a, Ord a, Hashable a) => ConstraintsADT a -> State (GCState a) [WQO a] -getConstraints' (Sat w) = return [w] -getConstraints' Unsat = return [] -getConstraints' c@(Union lhs rhs) = - cached c $ do - c1' <- cached c1 $ getConstraints' c1 - c2' <- cached c2 $ getConstraints' c2 - return $ c1' ++ c2' - where - (c1, c2) = - if cost lhs < cost rhs - then (lhs, rhs) - else (rhs, lhs) -getConstraints' c@(Intersect lhs rhs) = cached c $ do - c1' <- cached c1 $ getConstraints' c1 - if null c1' - then return [] - else (cached c2 $ getConstraints' c2) >>= go c1' - where - go :: [WQO a] -> [WQO a] -> State (GCState a) [WQO a] - go c1' c2' = flatten <$> - (sequence $ do - wqo1 <- c1' - wqo2 <- c2' - return (cached' (wqo1, wqo2) $ WQO.merge wqo1 wqo2)) - flatten = concatMap Mb.maybeToList - (c1, c2) = - if cost lhs > cost rhs - then (lhs, rhs) - else (rhs, lhs) - -dnfSize :: ConstraintsADT a -> Int -dnfSize (Sat w) = 1 -dnfSize Unsat = 0 -dnfSize (Union w1 w2) = dnfSize w1 + dnfSize w2 -dnfSize (Intersect w1 w2) = dnfSize w1 * dnfSize w2 - --- toDNF (Union lhs rhs) = S.union (toDNF lhs) (toDNF rhs) --- toDNF (Intersect lhs rhs) = --- let --- ldnf = toDNF lhs --- rdnf = toDNF rhs --- in --- S.unions - -simplify adt = undefined --- simplify adt = case getConstraints adt of --- [] -> Unsat --- (x:xs) -> foldl go (Sat x) xs --- where --- go a x = Union (Sat x) a - -permits adt wqo = any (`WQO.notStrongerThan` wqo) (getConstraints adt) - -isSatisfiable :: (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => ConstraintsADT a -> SMTExpr Bool -isSatisfiable s = toSMT s - -- trace (show (minDepth s) ++ " " ++ show (maxDepth s)) $ not $ null $ getConstraints s - -instance (Eq a, Hashable a, Show a) => Show (ConstraintsADT a) where - -- show s = go 0 s where - -- go n (Sat w) = indent n $ show w - -- go n Unsat = indent n $ "⊥" - -- go n (Union w t ) = indent n $ printf "∪\n%s\n%s" (go (n+1) w) (go (n+1) t) - -- go n (Intersect w t) = indent n $ printf "∩\n%s\n%s" (go (n+1) w) (go (n+1) t) - - -- indent 0 s = s - -- indent n s = take (n - 1) (repeat '|') ++ '+':s - - show (Sat w) = show w - show Unsat = "⊥" - show (Union w t ) = printf "(%s ∨\n %s)" (show w) (show t) - show (Intersect w t) = printf "(%s ∧ %s)" (show w) (show t) - -adtOC z3 = OC.liftC (checkSat' z3) adtOC' - -adtOC' = OC.OC - addConstraint - intersect - isSatisfiable - notStrongerThan - noConstraints - permits - relevantConstraints - union - unsatisfiable - undefined - undefined - simplify diff --git a/src/Language/REST/OrderingConstraints/Lazy.hs b/src/Language/REST/OrderingConstraints/Lazy.hs deleted file mode 100644 --- a/src/Language/REST/OrderingConstraints/Lazy.hs +++ /dev/null @@ -1,118 +0,0 @@ -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE ScopedTypeVariables #-} - -module Language.REST.OrderingConstraints.Lazy ( - lazyOC - , addConstraint - , intersect - , isSatisfiable - , noConstraints - , union - , unsatisfiable - , LazyOC - ) where - -import Debug.Trace -import Text.Printf -import GHC.Generics (Generic) -import Data.Hashable -import Data.Maybe -import qualified Data.List as L -import qualified Data.Set as S - -import qualified Language.REST.WQO as WQO -import qualified Language.REST.OrderingConstraints as OC -import qualified Language.REST.OrderingConstraints.ADT as ADT - -type WQO = WQO.WQO - --- Partially lazy ordering constraints: --- thunks computation after showing satisfiability - -type Thunk a = ADT.ConstraintsADT a - -data LazyOC a = - Unsat - | Sat (WQO a) (Thunk a) - deriving (Eq, Ord, Generic, Hashable) - -getOrdering (Sat wqo _) = Just wqo -getOrdering _ = Nothing - -eval :: (Eq a, Ord a, Hashable a) => ADT.ConstraintsADT a -> LazyOC a -eval (ADT.Sat w) = Sat w ADT.Unsat -eval ADT.Unsat = Unsat -eval (ADT.Union lhs rhs) = - case eval t1 of - Sat w t1' -> Sat w (ADT.union t1' t2) - Unsat -> eval t2 - where - (t1, t2) = (lhs, rhs) - -- if ADT.minDepth lhs < ADT.minDepth rhs - -- then (lhs, rhs) - -- else (rhs, lhs) - -eval (ADT.Intersect t1 t2) = - case (eval t1, eval t2) of - (Sat c1 t1', Sat c2 t2') -> - let - rest = - (ADT.intersect (ADT.Sat c1) t2') `ADT.union` - (ADT.intersect (ADT.Sat c2) t1') `ADT.union` - (ADT.intersect t1' t2') - in - case WQO.merge c1 c2 of - Just c' -> Sat c' rest - Nothing -> eval rest - _ -> Unsat - - -toADT Unsat = ADT.Unsat -toADT (Sat w r) = ADT.union (ADT.Sat w) r - -instance (Show a, Eq a, Ord a, Hashable a) => Show (LazyOC a) where - show Unsat = "⊥" - show (Sat s r) = printf "%s ∨ lazy(%s)" (show s) (show r) - -noConstraints = Sat (WQO.empty) ADT.Unsat -unsatisfiable = Unsat - -union Unsat s = s -union s Unsat = s -union (Sat s _) _ | s == WQO.empty = noConstraints -union _ (Sat s _) | s == WQO.empty = noConstraints -union (Sat s1 r1) (Sat s2 r2) = Sat s1 (ADT.union (ADT.Sat s2) (ADT.union r1 r2)) - -intersect t1 t2 = eval $ ADT.intersect (toADT t1) (toADT t2) - -isSatisfiable (Sat _ _) = True -isSatisfiable Unsat = False - -singleton c = Sat c ADT.Unsat - -relevantConstraints c _ _ = c - -notStrongerThan _ Unsat = return True -notStrongerThan t1 t2 = return $ t1 == t2 - -addConstraint o c = eval $ ADT.addConstraint o (toADT c) - -permits Unsat _ = False -permits (Sat s1 thunk) wqo = s1 `WQO.notStrongerThan` wqo || permits (eval thunk) wqo - -lazyOC :: Monad m => OC.OrderingConstraints LazyOC m -lazyOC = OC.OC - addConstraint - intersect - (return . isSatisfiable) - notStrongerThan - noConstraints - permits - relevantConstraints - union - unsatisfiable - undefined - getOrdering - id diff --git a/src/Language/REST/OrderingConstraints/Strict.hs b/src/Language/REST/OrderingConstraints/Strict.hs deleted file mode 100644 --- a/src/Language/REST/OrderingConstraints/Strict.hs +++ /dev/null @@ -1,152 +0,0 @@ -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE ScopedTypeVariables #-} - -module Language.REST.OrderingConstraints.Strict ( - strictOC - , strictOC' - , addConstraint - , difference - , getOrdering - , intersect - , isSatisfiable - , isUnsatisfiable - , noConstraints - , notStrongerThan - , permits - , relevantConstraints - , union - , unsatisfiable - , singleton - , StrictOC - , elems - ) where - -import Control.Monad.Identity -import Debug.Trace -import Text.Printf -import GHC.Generics (Generic) -import Data.Hashable -import Data.Maybe -import qualified Data.List as L -import qualified Data.Set as S - -import qualified Language.REST.OrderingConstraints as OC -import qualified Language.REST.WQO as WQO - -type WQO = WQO.WQO - --- Represents a set of constraints on a WQO on type `a` - --- The constraints are represented as a set ws of WQOs --- The constraints permit any WQO w that is a valid extension of some (w' in wqos) - - -data StrictOC a = StrictOC (S.Set (WQO a)) - deriving (Eq, Ord, Generic, Hashable) - -instance (Show a, Eq a, Ord a, Hashable a) => Show (StrictOC a) where - show (StrictOC cs) | S.null cs = "unsatisfiable" - show (StrictOC cs) | S.member WQO.empty cs = "no constraints" - show (StrictOC cs) = L.intercalate " ∨ \n" (map show (S.toList cs)) - -- where - -- show' o@(OpOrdering s) = if S.size s > 1 then printf "(%s)" (show o) else show o - -getOrdering :: StrictOC a -> Maybe (WQO a) -getOrdering (StrictOC o) = - listToMaybe (S.toList o) - -elems (StrictOC sets) = S.unions $ map WQO.elems (S.toList sets) - -noConstraints :: forall a. (Eq a, Ord a, Hashable a) => StrictOC a -noConstraints = StrictOC (S.singleton (WQO.empty)) - -unsatisfiable = StrictOC S.empty - -isUnsatisfiable :: Eq a => StrictOC a -> Bool -isUnsatisfiable c = c == unsatisfiable - -isSatisfiable :: Eq a => StrictOC a -> Bool -isSatisfiable c = c /= unsatisfiable - -notStrongerThan :: forall m a. (Monad m, Eq a, Ord a, Hashable a) => StrictOC a -> StrictOC a -> m Bool -notStrongerThan (StrictOC lhs) (StrictOC rhs) = return False - --- The difference of two constraints `a` and `b` is new constraints such that --- intersect (diff a b) b = a -difference :: (Eq a, Ord a, Hashable a) => StrictOC a -> StrictOC a -> StrictOC a -difference (StrictOC lhs) (StrictOC rhs) = - StrictOC (S.difference lhs rhs) - --- The union of two constraints `a` and `b` is new constraints that only --- permits an ordering if permitted by either `a` or `b` -union :: (Eq a, Ord a, Hashable a) => StrictOC a -> StrictOC a -> StrictOC a -union (StrictOC lhs) (StrictOC rhs) = - fromSet $ S.union lhs rhs - -fromSet :: (Eq a, Ord a, Hashable a) => S.Set (WQO a) -> StrictOC a -fromSet oc = -- StrictOC oc - StrictOC $ go [] (L.sortOn (length . WQO.elems) $ S.toList oc) - where - go include [] = S.fromList include - go include (x : xs) = - if any (`WQO.notStrongerThan` x) (include ++ xs) - then go include xs - else go (x : include) xs - - --- The intersection of two constraints `a` and `b` is new constraints that only --- permits the orderings permitted by both `a` and `b` -intersect :: (Show a, Eq a, Ord a, Hashable a) => StrictOC a -> StrictOC a -> StrictOC a -intersect (StrictOC lhs) (StrictOC rhs) = result - -- trace (printf "%s intersect %s yields %s" (show lhs) (show rhs) (show result)) result - where - result = fromSet $ S.fromList $ - do - lhs' <- S.toList lhs - rhs' <- S.toList rhs - maybeToList (WQO.merge lhs' rhs') - -addConstraint :: (Eq a, Ord a, Hashable a) => WQO a -> StrictOC a -> StrictOC a -addConstraint c (StrictOC oc) = StrictOC $ S.fromList $ do - c' <- S.toList oc - maybeToList $ WQO.merge c c' - -singleton :: (Eq a, Ord a, Hashable a) => WQO a -> StrictOC a -singleton c = addConstraint c noConstraints - -relevantConstraints :: forall a. (Eq a, Ord a, Hashable a) => StrictOC a -> S.Set a -> S.Set a -> StrictOC a -relevantConstraints (StrictOC oc0) as bs = go (S.toList oc0) unsatisfiable - where - go :: [WQO a] -> StrictOC a -> StrictOC a - go [] oc = oc - go (o : rest) exist = - let - o' = WQO.relevantTo o as bs - in - if WQO.null o' - then noConstraints - else go rest (union (singleton o) exist) - -permits :: (Eq a, Ord a, Hashable a) => StrictOC a -> WQO a -> Bool -permits (StrictOC permitted) desired = - any (`WQO.notStrongerThan` desired) (S.toList permitted) - -strictOC :: Monad m => OC.OrderingConstraints StrictOC m -strictOC = OC.OC - addConstraint - intersect - (return . isSatisfiable) - notStrongerThan - noConstraints - permits - relevantConstraints - union - unsatisfiable - elems - getOrdering - id - -strictOC' :: OC.OrderingConstraints StrictOC Identity -strictOC' = strictOC diff --git a/src/Language/REST/PartialOrder.hs b/src/Language/REST/PartialOrder.hs deleted file mode 100644 --- a/src/Language/REST/PartialOrder.hs +++ /dev/null @@ -1,98 +0,0 @@ -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveAnyClass #-} - -module Language.REST.PartialOrder ( - empty - , insert - , replaceUnsafe - , insertUnsafe - , gt - , toList - , isEmpty - , elems - , unionDisjointUnsafe - , PartialOrder - , toDescsList - , descendents - ) where - -import GHC.Generics (Generic) -import Debug.Trace -import Data.Hashable -import qualified Data.Set as S -import qualified Data.Map as M -import qualified Data.List as L - -import Language.REST.Types -import Text.Printf - -newtype PartialOrder a = PartialOrder (M.Map a (S.Set a)) - deriving (Ord, Eq, Generic, Hashable) - -instance (Show a) => Show (PartialOrder a) where - show (PartialOrder m) = L.intercalate " ∧ " $ map go (M.toList m) where - go (key, s) = case S.toList s of - [x] -> printf "%s > %s" (show key) (show x) - xs -> printf "%s > { %s }" (show key) (L.intercalate ", " (map show xs)) - - -empty = PartialOrder M.empty - -isEmpty p = p == empty - -canInsert :: (Eq a, Ord a, Hashable a) => PartialOrder a -> a -> a -> Bool -canInsert o f g = f /= g && not (gt o f g) && not (gt o g f) - -gt :: (Eq a, Ord a, Hashable a) => PartialOrder a -> a -> a -> Bool -gt po t u = S.member u $ descendents t po - -unionDisjointUnsafe (PartialOrder m) (PartialOrder m') = PartialOrder (M.union m m') - -ascendants k (PartialOrder m) = M.keysSet $ M.filter (S.member k) m -descendents k (PartialOrder m) = M.findWithDefault S.empty k m - -{-# INLINE insertUnsafe #-} -insertUnsafe o@(PartialOrder m) f g = result - where - result = PartialOrder $ M.insertWith S.union f decs $ M.mapWithKey go m - - go k old | S.member k ascs = S.union old decs - go _ v | otherwise = v - - ascs = ascendants f o - decs = S.insert g $ descendents g o - -{-# INLINE insert #-} -insert :: (Eq a, Ord a, Hashable a) => PartialOrder a -> a -> a -> Maybe (PartialOrder a) -insert o f g = if canInsert o f g then Just (insertUnsafe o f g) else Nothing - -toDescsList (PartialOrder m) = M.toList m - -toList :: PartialOrder a -> [(a, a)] -toList (PartialOrder m) = do - (k, vs) <- M.toList m - v <- S.toList vs - return (k, v) - -elems :: (Eq a, Ord a, Hashable a) => PartialOrder a -> S.Set a -elems (PartialOrder m) = S.union (M.keysSet m) (S.unions (M.elems m)) - -replaceUnsafe :: (Eq a, Ord a, Hashable a) => [a] -> a -> PartialOrder a -> PartialOrder a -replaceUnsafe froms to po@(PartialOrder m) = result where - - from' = S.fromList froms - - descs = S.unions (map (`descendents` po) froms) - - filtered = M.filterWithKey (\k _ -> not $ k `elem` froms) m - m' = - if S.null descs - then filtered - else M.insertWith S.union to descs filtered - - result = PartialOrder $ M.map go m' - - go s | hasFrom s = S.insert to $ S.union descs $ S.difference s from' - go s | otherwise = s - - hasFrom set = any (`S.member` set) froms diff --git a/src/Language/REST/Path.hs b/src/Language/REST/Path.hs --- a/src/Language/REST/Path.hs +++ b/src/Language/REST/Path.hs @@ -7,7 +7,6 @@ import qualified Data.HashSet as S import GHC.Generics (Generic) import Data.Hashable -import Language.REST.Types data Step rule term a = Step { term :: PathTerm rule term diff --git a/src/Language/REST/ProofGen.hs b/src/Language/REST/ProofGen.hs deleted file mode 100644 --- a/src/Language/REST/ProofGen.hs +++ /dev/null @@ -1,55 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -module Language.REST.ProofGen where - -import qualified Data.HashMap.Strict as M -import qualified Data.List as L -import qualified Data.Text as T -import Text.Printf - -import Language.REST.Path -import Language.REST.Rewrite -import Language.REST.RuntimeTerm -import Language.REST.Op - --- Hardcoded -opToLH (Op "union") = "mp" -opToLH (Op "toMS") = "multiset_of" -opToLH (Op op) = T.unpack op - -withParens True t = "(" ++ t ++ ")" -withParens False t = t - -toLH :: Bool -> RuntimeTerm -> String --- Hardcoded rules -toLH parens (App "m" [arg]) = withParens parens $ printf "Multiset [%s]" (toLH False arg) -toLH parens (App "cons" [x, xs]) = withParens parens $ printf "%s:%s" (toLH True x) (toLH True xs) - -toLH _ (App op []) = opToLH op -toLH parens (App op args) = - withParens parens $ printf "%s %s" (opToLH op) (L.intercalate " " $ map (toLH True) args) - -toProof :: Path Rewrite RuntimeTerm a -> String -toProof (steps, PathTerm result _) = " " ++ (L.intercalate "\n=== " $ proofSteps ++ [toLH False result]) ++ "\n*** QED" - where - proofSteps :: [String] - proofSteps = map proofStep $ zip steps [0..] - - proofStep ((Step (PathTerm t _) _ _ True), _) = toLH False t - proofStep ((Step (PathTerm t _) (Rewrite lhs rhs name) _ False), i) = toLH False t ++ " ? " ++ toLemma lemma - where - lemma = go (subTerms t) - - lemmaName = - case name of - Just n -> T.pack n - Nothing -> "lemma" - - toLemma s = toLH False (App (Op lemmaName) (map snd $ L.sort $ M.toList s)) - - go [] = undefined - go ((st, f): _) | Just su <- unify lhs st M.empty - , f (subst su rhs) == nextTerm - = su - go (_:xs) = go xs - - nextTerm = if i < (length steps - 1) then (pathTerm . term) (steps !! (i + 1)) else result diff --git a/src/Language/REST/RESTDot.hs b/src/Language/REST/RESTDot.hs --- a/src/Language/REST/RESTDot.hs +++ b/src/Language/REST/RESTDot.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} module Language.REST.RESTDot where @@ -9,7 +10,6 @@ import Language.REST.Dot import Language.REST.Path -import Language.REST.Types data PrettyPrinter rule term ord = PrettyPrinter { printRule :: rule -> String @@ -24,10 +24,10 @@ rejectedNodes :: forall rule term a . (Hashable rule, Hashable term, Hashable a) => GraphType -> PrettyPrinter rule term a -> Path rule term a -> S.Set Node rejectedNodes _ pp _ | not (showRejects pp) = S.empty -rejectedNodes gt pp p@(steps, (PathTerm _ rejected)) = S.fromList $ map go (HS.toList rejected) +rejectedNodes gt pp p@(_steps, (PathTerm {rejected})) = S.fromList $ map go (HS.toList rejected) where go :: (term, rule) -> Node - go (term, r) = Node (rejNodeID gt p term) (printTerm pp term) "dashed" "red" + go (rejTerm, _r) = Node (rejNodeID gt p rejTerm) (printTerm pp rejTerm) "dashed" "red" getNodeID :: (Hashable rule, Hashable term, Hashable a) => GraphType -> Path rule term a -> String @@ -41,9 +41,9 @@ => GraphType -> PrettyPrinter rule term a -> Path rule term a -> Node endNode gt pp p@(_, t) = let - nodeID = getNodeID gt p + thisNodeID = getNodeID gt p in - Node nodeID (printTerm pp (pathTerm t)) "solid" "black" + Node thisNodeID (printTerm pp (pathTerm t)) "solid" "black" toEdges :: forall rule term a . (Hashable rule, Hashable term, Hashable a) => GraphType -> PrettyPrinter rule term a -> Path rule term a -> S.Set Edge @@ -59,8 +59,8 @@ then S.fromList $ map go (HS.toList rej) else S.empty where - go (term, r) = - Edge (nodeID (endNode gt pp p)) (rejNodeID gt p term) (printRule pp r) "red" " " "dotted" + go (rejTerm, r) = + Edge (nodeID (endNode gt pp p)) (rejNodeID gt p rejTerm) (printRule pp r) "red" " " "dotted" toEdge :: (Path rule term a, Path rule term a) -> Edge @@ -68,16 +68,16 @@ let step = last ts color = if (fromPLE step) then "brown" else "darkgreen" - subLabel = printOrd pp (ordering step) + esubLabel = printOrd pp (ordering step) startNodeID = nodeID (endNode gt pp p0) endNodeID = nodeID (endNode gt pp p1) in - Edge startNodeID endNodeID (printRule pp (rule step)) color subLabel "solid" + Edge startNodeID endNodeID (printRule pp (rule step)) color esubLabel "solid" subPaths :: Path rule term a -> [Path rule term a] -subPaths p@(xs, t) = map toPath (tail $ inits xs) ++ [p] +subPaths p@(xs, _t) = map toPath (tail $ inits xs) ++ [p] where - toPath xs = (init xs, term (last xs)) + toPath ys = (init ys, term (last ys)) toNodes :: (Hashable rule, Hashable term, Hashable a) => GraphType -> PrettyPrinter rule term a -> Path rule term a -> S.Set Node toNodes gt pp path = diff --git a/src/Language/REST/RPO.hs b/src/Language/REST/RPO.hs --- a/src/Language/REST/RPO.hs +++ b/src/Language/REST/RPO.hs @@ -9,29 +9,22 @@ module Language.REST.RPO (rpo, rpoTerm, rpoGTE, rpoGTE', synGTE) where import Prelude hiding (EQ, GT) -import Debug.Trace (trace) -import Text.Printf import Control.Monad.Identity import Control.Monad.State.Strict import GHC.Generics import Data.Hashable -import qualified Data.List as L -import qualified Data.HashSet as S import qualified Data.HashMap.Strict as M -import qualified Language.REST.MultiSet as MS +import qualified Language.REST.Internal.MultiSet as MS import Language.REST.Op -import Language.REST.OpOrdering as OpOrdering -import Language.REST.OrderingConstraints as OC +import Language.REST.Internal.OpOrdering as OpOrdering +import Language.REST.WQOConstraints as OC import qualified Language.REST.MetaTerm as MT import Language.REST.Types import qualified Language.REST.RuntimeTerm as RT -import Language.REST.MultisetOrder - -type MultiSet = MS.MultiSet - -data RuntimeTerm = App Op (MultiSet RuntimeTerm) deriving (Generic, Eq, Hashable, Ord) +import Language.REST.Internal.MultisetOrder +import Language.REST.Internal.Util instance Show RuntimeTerm where show (App op trms) = @@ -42,19 +35,16 @@ instance MT.ToMetaTerm RuntimeTerm where toMetaTerm (App op xs) = MT.RWApp op (map MT.toMetaTerm $ MS.toList xs) -ops :: RuntimeTerm -> S.HashSet Op -ops (App f ts) = S.insert f (S.unions $ map ops (MS.distinctElems ts)) +type MultiSet = MS.MultiSet +data RuntimeTerm = App Op (MultiSet RuntimeTerm) deriving (Generic, Eq, Hashable, Ord) + rpoTerm :: RT.RuntimeTerm -> RuntimeTerm rpoTerm (RT.App f xs) = App f $ MS.fromList (map rpoTerm xs) isSubtermOf :: RuntimeTerm -> RuntimeTerm -> Bool isSubtermOf t u@(App _ us) = t == u || any (t `isSubtermOf`) (MS.distinctElems us) -trace' :: String -> a -> a --- trace' = trace -trace' _ x = x - type CacheKey oc = ((oc Op), Relation, RuntimeTerm, RuntimeTerm) type Cache oc = M.HashMap (CacheKey oc) (oc Op) @@ -76,19 +66,15 @@ cached :: (Eq (oc Op), Hashable (oc Op)) => CacheKey oc -> RMonad oc (oc Op) -> RMonad oc (oc Op) -cached key@(_,_,t1,t2) thunk = do +cached key thunk = do cache <- gets rpoCache case M.lookup key cache of - Just result -> trace' ("Cache hit" ++ show (t1, t2)) $ return result - Nothing -> trace' ("Cache miss" ++ show (t1, t2)) $ do - result <- trace' "Do thunk" thunk - trace' "Done" $ modify (\st -> st{ rpoCache = M.insert key result (rpoCache st)}) + Just result -> return result + Nothing -> do + result <- thunk + modify (\st -> st{ rpoCache = M.insert key result (rpoCache st)}) return result - where - trace' _ x = x - -- trace' = trace - rpo :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RT.RuntimeTerm Identity rpo = runStateConstraints (cmapConstraints rpoTerm rpo') (RPOState M.empty 0) @@ -100,61 +86,49 @@ rpo' OC{unsatisfiable} r oc t u | t == u = return $ if r == GT then unsatisfiable else oc rpo' OC{unsatisfiable} _ _ t u | t `isSubtermOf` u = return unsatisfiable rpo' OC{unsatisfiable} r oc t u | u `isSubtermOf` t = return $ if r == EQ then unsatisfiable else oc -rpo' oc r cs t@(App f ts) u@(App g us) | f == g = rpoMul oc r cs ts us +rpo' oc r cs (App f ts) (App g us) | f == g = rpoMul oc r cs ts us rpo' oc r cs t@(App f ts) u@(App g us) = incDepth result where - traceString depth = printf "%s %s %s %s" (take depth $ repeat '.') (show t) (show r) (show u) - cs' = noConstraints oc -- relevantConstraints oc cs (ops t) (ops u) + cs' = noConstraints oc result = cached (cs, r, t, u) $ (intersect oc cs <$> result') - result' = cached (cs', r, t, u) $ do - depth <- gets rpoDepth - trace' (traceString depth) $ - if r == EQ - then rpoMul oc r (addConstraint oc (f =. g) cs') ts us - else - unionAll oc <$> sequence [ - rpoMul oc GT (addConstraint oc (f >. g) cs') (MS.singleton t) us - , rpoMul oc r (addConstraint oc (f =. g) cs') ts us - , rpoMul oc GTE cs' ts (MS.singleton u) - ] - - + result' = cached (cs', r, t, u) $ + if r == EQ + then rpoMul oc r (addConstraint oc (f =. g) cs') ts us + else + unionAll oc <$> sequence [ + rpoMul oc GT (addConstraint oc (f >. g) cs') (MS.singleton t) us + , rpoMul oc r (addConstraint oc (f =. g) cs') ts us + , rpoMul oc GTE cs' ts (MS.singleton u) + ] +rpoGTE + :: (?impl::WQOConstraints oc m, Hashable (oc Op), Eq (oc Op), Show (oc Op)) + => RT.RuntimeTerm + -> RT.RuntimeTerm + -> oc Op rpoGTE t u = runIdentity $ rpoGTE' ?impl (noConstraints ?impl) t u +rpoGTE' + :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) + => WQOConstraints oc m' + -> oc Op + -> RT.RuntimeTerm + -> RT.RuntimeTerm + -> Identity (oc Op) rpoGTE' impl oc t u = rpo impl GTE oc t u - - - - - - - - - - - -- Non symbolic version synEQ :: OpOrdering -> RuntimeTerm -> RuntimeTerm -> Bool synEQ o l r = synGTE' o l r && synGTE' o r l -removeSynEQs :: OpOrdering -> [RuntimeTerm] -> [RuntimeTerm] -> ([RuntimeTerm], [RuntimeTerm]) -removeSynEQs _ [] ys = ([], ys) -removeSynEQs ordering (x : xs) ys - | Just y <- L.find (synEQ ordering x) ys - = removeSynEQs ordering xs $ L.delete y ys - | otherwise - = let (xs', ys') = removeSynEQs ordering xs ys in (x : xs', ys') - synGTE :: OpOrdering -> RT.RuntimeTerm -> RT.RuntimeTerm -> Bool synGTE o t u = synGTE' o (rpoTerm t) (rpoTerm u) synGTE' :: OpOrdering -> RuntimeTerm -> RuntimeTerm -> Bool -synGTE' ordering t@(App f ts) u@(App g us) +synGTE' ordering t@(App f _ts) (App g us) | opGT ordering f g = synGTM ordering (MS.singleton t) us synGTE' ordering (App f ts) (App g us) @@ -166,10 +140,10 @@ rpoT o t1 t2 = synGTE' o t1 t2 && not (synGTE' o t2 t1) synGTEM :: OpOrdering -> MultiSet RuntimeTerm -> MultiSet RuntimeTerm -> Bool -synGTEM ordering xs ys = case removeSynEQs ordering (MS.toList xs) (MS.toList ys) of +synGTEM ordering xs ys = case removeEqBy (synEQ ordering) (MS.toList xs) (MS.toList ys) of (xs', ys') -> all (\y -> any (\x -> rpoT ordering x y) xs') ys' synGTM :: OpOrdering -> MultiSet RuntimeTerm -> MultiSet RuntimeTerm -> Bool -synGTM ordering xs ys = case removeSynEQs ordering (MS.toList xs) (MS.toList ys) of +synGTM ordering xs ys = case removeEqBy (synEQ ordering) (MS.toList xs) (MS.toList ys) of ([] , [] ) -> False (xs', ys') -> all (\y -> any (\x -> rpoT ordering x y) xs') ys' diff --git a/src/Language/REST/Rest.hs b/src/Language/REST/Rest.hs --- a/src/Language/REST/Rest.hs +++ b/src/Language/REST/Rest.hs @@ -4,6 +4,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE NamedFieldPuns #-} +{-# OPTIONS_GHC -Wno-error=deprecations #-} module Language.REST.Rest ( rest @@ -22,21 +23,21 @@ import qualified Data.List as L import qualified Data.HashMap.Strict as M import qualified Data.Maybe as Mb -import Debug.Trace -import Text.Printf -import Language.REST.AbstractOC as AC +import Language.REST.OCAlgebra as AC import Language.REST.RewriteRule import Language.REST.Path -import Language.REST.Types import Language.REST.ExploredTerms as ET -import Language.REST.WorkStrategy +import Language.REST.Internal.WorkStrategy newtype PathsResult rule term oc = PathsResult (S.HashSet (Path rule term oc)) newtype TermsResult rule term oc = TermsResult (S.HashSet term) +pathsResult :: PathsResult rule term oc pathsResult = PathsResult S.empty + +termsResult :: TermsResult rule term oc termsResult = TermsResult S.empty class RESTResult a where @@ -66,8 +67,9 @@ , toET :: term -> et , target :: Maybe term , workStrategy :: WorkStrategy rule term et oc - , ocImpl :: AbstractOC oc term m + , ocImpl :: OCAlgebra oc term m , initRes :: rtype rule term oc + , etStrategy :: ExploreStrategy } rest :: forall m rule term oc et rtype . @@ -87,11 +89,11 @@ => RESTParams m rule term oc et rtype -> term -> m ((rtype rule term oc), Maybe (Path rule term oc)) -rest RESTParams{re,ru,toET,ocImpl,workStrategy,initRes,target} t = +rest RESTParams{re,ru,toET,ocImpl,workStrategy,initRes,target,etStrategy} t = rest' (RESTState initRes [([], PathTerm t S.empty)] initET Nothing) where (WorkStrategy ws) = workStrategy - initET = ET.empty $ EF (AC.union ocImpl) (AC.notStrongerThan ocImpl) + initET = ET.empty (EF (AC.union ocImpl) (AC.notStrongerThan ocImpl)) etStrategy rest' (RESTState fin [] _ targetPath) = return (fin, targetPath) rest' state@(RESTState _ paths et (Just targetPath)) @@ -99,10 +101,10 @@ , length steps >= length (fst targetPath) = rest' state{working = remaining} rest' state@(RESTState fin paths et targetPath) = do - se <- shouldExplore (toET t) lastOrdering et + se <- shouldExplore (toET ptTerm) lastOrdering et if se then do - evalRWs <- candidates re -- trace ("Explore " ++ (show $ toET t)) $ candidates re + evalRWs <- candidates re userRWs <- candidates ru acceptedUserRWs <- accepted userRWs go evalRWs userRWs acceptedUserRWs @@ -110,7 +112,7 @@ rest' (state{ working = remaining }) where - (path@(ts, PathTerm t _), remaining) = ws paths toET et + (path@(ts, PathTerm ptTerm _), remaining) = ws paths toET et lastOrdering :: oc lastOrdering = if L.null ts then top ocImpl else ordering $ last ts @@ -127,14 +129,14 @@ res :: m [(term, rule)] res = runListT $ do r <- liftSet rules - t' <- ListT $ S.toList <$> apply t r + t' <- ListT $ S.toList <$> apply ptTerm r return (t', r) accepted :: (S.HashSet (term, rule)) -> m (M.HashMap term oc) accepted userRWs = M.fromList <$> (runListT $ do t' <- liftSet $ S.map fst userRWs guard $ L.notElem t' tsTerms - let ord = refine ocImpl lastOrdering t t' + let ord = refine ocImpl lastOrdering ptTerm t' ok <- lift $ isSat ocImpl ord guard ok return (t', ord)) @@ -153,9 +155,9 @@ let deps = S.map (toET . fst) (S.union evalRWs userRWs) in - ET.insert (toET t) lastOrdering deps et + ET.insert (toET ptTerm) lastOrdering deps et , targetPath = - if Just t == target then + if Just ptTerm == target then case targetPath of Just (tp, _) | length tp <= length ts -> targetPath _ -> Just (ts, pt) @@ -164,7 +166,7 @@ } - pt = PathTerm t rejectedUserRewrites + pt = PathTerm ptTerm rejectedUserRewrites rejectedUserRewrites :: S.HashSet (term, rule) rejectedUserRewrites = S.fromList $ do @@ -177,7 +179,7 @@ evalPaths = runListT $ do (t', r) <- ListT $ return (S.toList evalRWs) guard $ L.notElem t' tsTerms - let ord = refine ocImpl lastOrdering t t' + let ord = refine ocImpl lastOrdering ptTerm t' lift (shouldExplore (toET t') ord et) >>= guard return (ts ++ [Step pt r ord True], PathTerm t' S.empty) diff --git a/src/Language/REST/Rewrite.hs b/src/Language/REST/Rewrite.hs deleted file mode 100644 --- a/src/Language/REST/Rewrite.hs +++ /dev/null @@ -1,56 +0,0 @@ -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} - -module Language.REST.Rewrite where - -import GHC.Generics (Generic) - -import Control.Monad.Identity -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 (Eq, Ord, Generic, Hashable, Show) - -type Subst = M.HashMap String RuntimeTerm - -getName (Rewrite t u n) = n -named (Rewrite t u _) n = Rewrite t u (Just n) - -subst :: Subst -> MetaTerm -> RuntimeTerm -subst s (MT.Var v) | Just t <- M.lookup v s = t - | otherwise - = error $ printf "No value for metavar %s during subst %s" (show v) (show s) -subst s (MT.RWApp op xs) = App op (map (subst s) xs) - -unifyAll :: Subst -> [(MetaTerm, RuntimeTerm)] -> Maybe Subst -unifyAll su [] = Just su -unifyAll su ((x, y) : ts) - | Just s <- unify x y su - = unifyAll s ts - | otherwise - = Nothing - -unify :: MetaTerm -> RuntimeTerm -> Subst -> Maybe Subst -unify (MT.Var s) term su | M.lookup s su == Just term - = Just su -unify (MT.Var s) term su | M.lookup s su == Nothing - = Just $ M.insert s term su -unify (MT.RWApp o1 xs) (App o2 ys) su | o1 == o2 && length xs == length ys = - unifyAll su (zip xs ys) -unify _ _ _ = Nothing - -instance Monad m => RewriteRule m Rewrite RuntimeTerm where - apply t (Rewrite left right _) = return $ S.unions $ map go (subTerms t) - where - go (t', tf) | Just su <- unify left t' M.empty = S.singleton (tf $ subst su right) - go _ | otherwise = S.empty diff --git a/src/Language/REST/RuntimeTerm.hs b/src/Language/REST/RuntimeTerm.hs --- a/src/Language/REST/RuntimeTerm.hs +++ b/src/Language/REST/RuntimeTerm.hs @@ -31,9 +31,9 @@ st :: Int -> [(RuntimeTerm, (RuntimeTerm -> RuntimeTerm))] st i = let - t = ts !! i + ti = ts !! i go t' = App f $ take i ts ++ [t'] ++ drop (i + 1) ts - go2 (st, toFull) = (st, go . toFull) + go2 (srt, toFull) = (srt, go . toFull) in - map go2 (subTerms t) + map go2 (subTerms ti) diff --git a/src/Language/REST/SMT.hs b/src/Language/REST/SMT.hs --- a/src/Language/REST/SMT.hs +++ b/src/Language/REST/SMT.hs @@ -1,77 +1,211 @@ {-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GADTs #-} -{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE InstanceSigs #-} -{-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UndecidableInstances #-} module Language.REST.SMT where import Control.Monad.IO.Class +import Data.Hashable +import qualified Data.Map as M import qualified Data.List as L import qualified Data.Set as S import qualified Data.Text as T import System.Process -import Text.Printf +import Text.Parsec (endBy) +import Text.Parsec.Prim +import Text.ParserCombinators.Parsec.Char +import GHC.Generics (Generic) import GHC.IO.Handle -newtype SMTVar = SMTVar T.Text deriving (Eq, Ord) +type Z3Model = M.Map String String +parens :: Text.Parsec.Prim.Stream s m Char => ParsecT s u m a -> ParsecT s u m a +parens p = do + _ <- char '(' + r <- p + _ <- char ')' + return r + +parseFunDef :: Text.Parsec.Prim.Stream s m Char => ParsecT s u m (String, String) +parseFunDef = parens $ do + _ <- string "define-fun " + var <- many (noneOf " ") + _ <- spaces + _ <- many (noneOf " ") -- args + _ <- spaces + _ <- many (noneOf " ") -- type + _ <- spaces + value <- many (noneOf ")") + return (var, value) + +modelParser :: Text.Parsec.Prim.Stream s m Char => ParsecT s u m Z3Model +modelParser = parens $ do + spaces + defs <- endBy parseFunDef spaces + return $ M.fromList defs + +readModel :: Handle -> IO String +readModel handle = go "" where + closedTerm t = length (filter (== '(') t) == length (filter (== ')') t) + go buf = do + line <- hGetLine handle + let buf' = buf ++ line ++ "\n" + if closedTerm buf' + then return buf' + else go buf' + +parseModel :: String -> Z3Model +parseModel str = case parse modelParser "" str of + Left err -> error (show err) + Right t -> t + +newtype SMTVar a = SMTVar T.Text deriving (Eq, Ord) + data SMTExpr a where And :: [SMTExpr Bool] -> SMTExpr Bool + Add :: [SMTExpr Int] -> SMTExpr Int Or :: [SMTExpr Bool] -> SMTExpr Bool Equal :: [SMTExpr a] -> SMTExpr Bool Greater :: SMTExpr Int -> SMTExpr Int -> SMTExpr Bool + GTE :: SMTExpr Int -> SMTExpr Int -> SMTExpr Bool Implies :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool - Var :: SMTVar -> SMTExpr a + Var :: SMTVar a -> SMTExpr a + Const :: Int -> SMTExpr Int -vars :: SMTExpr a -> S.Set SMTVar -vars (And ts) = S.unions (map vars ts) -vars (Or ts) = S.unions (map vars ts) -vars (Equal ts) = S.unions (map vars ts) -vars (Greater t u) = S.union (vars t) (vars u) -vars (Var var) = S.singleton var + +data UntypedExpr = + UAnd [UntypedExpr] + | UAdd [UntypedExpr] + | UOr [UntypedExpr] + | UEqual [UntypedExpr] + | UGreater UntypedExpr UntypedExpr + | UGTE UntypedExpr UntypedExpr + | UImplies UntypedExpr UntypedExpr + | UVar T.Text + | UConst Int + deriving (Show, Eq, Ord, Hashable, Generic) + +toUntyped :: SMTExpr a -> UntypedExpr +toUntyped (And xs) = UAnd (map toUntyped xs) +toUntyped (Add xs) = UAdd (map toUntyped xs) +toUntyped (Or xs) = UOr (map toUntyped xs) +toUntyped (Equal xs) = UEqual (map toUntyped xs) +toUntyped (Greater t u) = UGreater (toUntyped t) (toUntyped u) +toUntyped (GTE t u) = UGTE (toUntyped t) (toUntyped u) +toUntyped (Implies t u) = UImplies (toUntyped t) (toUntyped u) +toUntyped (Var (SMTVar text)) = UVar text +toUntyped (Const i) = UConst i + +instance (Eq (SMTExpr a)) where + t == u = toUntyped t == toUntyped u + +instance (Ord (SMTExpr a)) where + t <= u = toUntyped t <= toUntyped u + +instance Hashable (SMTExpr a) where + hashWithSalt salt e = hashWithSalt salt (toUntyped e) + +instance Show (SMTExpr a) where + show = T.unpack . toFormula + + +toFormula :: SMTExpr a -> T.Text +toFormula = go False where + go :: Bool -> SMTExpr a -> T.Text + go _ (And []) = "⊤" + go p (And ts) = eparens p $ T.intercalate " ∧ " $ map (go (not p)) ts + go p (Add ts) = eparens p $ T.intercalate " + " $ map (go (not p)) ts + go p (GTE t u) = eparens p $ T.intercalate " ≥ " $ map (go True) $ [t, u] + go p (Greater t u) = eparens p $ T.intercalate " > " $ map (go True) $ [t, u] + go _ (Var (SMTVar v)) = v + go _ (Const c) = T.pack (show c) + go _ _e = undefined + + eparens True t = T.concat ["(", t, ")"] + eparens False t = t + +vars :: SMTExpr a -> S.Set T.Text +vars (And ts) = S.unions (map vars ts) +vars (Add ts) = S.unions (map vars ts) +vars (Or ts) = S.unions (map vars ts) +vars (Equal ts) = S.unions (map vars ts) +vars (Greater t u) = S.union (vars t) (vars u) +vars (GTE t u) = S.union (vars t) (vars u) +vars (Var (SMTVar var)) = S.singleton var vars (Implies e1 e2) = S.union (vars e1) (vars e2) +vars (Const _) = S.empty -data SMTCommand = SMTAssert (SMTExpr Bool) | DeclareVar SMTVar | CheckSat | Push | Pop +data SMTCommand = SMTAssert (SMTExpr Bool) | DeclareVar T.Text | CheckSat | Push | Pop +smtFalse :: SMTExpr Bool smtFalse = Or [] + smtTrue :: SMTExpr Bool smtTrue = And [] +smtAdd :: [SMTExpr Int] -> SMTExpr Int +smtAdd [] = Const 0 +smtAdd ts = Add ts + +smtAnd :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool +smtAnd (And xs) (And ys) = And $ L.nub (xs ++ ys) +smtAnd (And xs) e = And $ L.nub (xs ++ [e]) +smtAnd e (And ys) = And $ L.nub (e:ys) +smtAnd t u = And [t, u] + +smtGTE :: SMTExpr Int -> SMTExpr Int -> SMTExpr Bool +smtGTE t u | t == u = smtTrue +smtGTE t u | otherwise = GTE t u + +app :: T.Text -> [SMTExpr a] -> T.Text app op trms = T.concat $ ["(", op, " ", (T.intercalate " " (map exprString trms)), ")"] exprString :: SMTExpr a -> T.Text -exprString (And []) = "true" -exprString (Or []) = "false" +exprString (And []) = "true" +exprString (Add es) = app "+" es +exprString (Or []) = "false" +exprString (And es) = app "and" es +exprString (Or es) = app "or" es exprString (Equal xs) | length xs < 2 = "true" -exprString (And es) = app "and" es -exprString (Or es) = app "or" es -exprString (Equal es) = app "=" es -exprString (Greater e1 e2) = app ">" [e1, e2] -exprString (Implies e1 e2) = app "=>" [e1, e2] +exprString (Equal es) = app "=" es +exprString (Greater e1 e2) = app ">" [e1, e2] +exprString (GTE e1 e2) = app ">=" [e1, e2] +exprString (Implies e1 e2) = app "=>" [e1, e2] exprString (Var (SMTVar var)) = var +exprString (Const i) = T.pack (show i) +commandString :: SMTCommand -> T.Text commandString (SMTAssert expr) = app "assert" [expr] -commandString (DeclareVar (SMTVar var)) = T.concat $ ["(declare-const ", var, " Int)"] +commandString (DeclareVar var) = T.concat $ ["(declare-const ", var, " Int)"] commandString CheckSat = "(check-sat)" commandString Push = "(push)" commandString Pop = "(pop)" askCmds :: SMTExpr Bool -> [SMTCommand] -askCmds expr = [Push] ++ varDecls ++ [SMTAssert expr, CheckSat, Pop] where +askCmds expr = varDecls ++ [SMTAssert expr, CheckSat] where varDecls = map DeclareVar $ S.toList (vars expr) type SolverHandle = (Handle, Handle) +spawnZ3 :: IO (Handle, Handle) spawnZ3 = do (Just stdIn, Just stdOut, _, _) <- createProcess (proc "z3" ["-in"]) {std_in = CreatePipe, std_out = CreatePipe} return (stdIn, stdOut) +killZ3 :: (Handle, b) -> IO () killZ3 (stdIn, _) = hClose stdIn +withZ3 :: MonadIO m => ((Handle, Handle) -> m b) -> m b withZ3 f = do z3 <- liftIO $ spawnZ3 @@ -79,17 +213,29 @@ liftIO $ killZ3 z3 return result +getModel :: Handle -> IO () +getModel stdIn = do + hPutStr stdIn "(get-model)\n" + hFlush stdIn + checkSat' :: (Handle, Handle) -> SMTExpr Bool -> IO Bool checkSat' (stdIn, stdOut) expr = do - hPutStr stdIn prog - hFlush stdIn + sendCommands $ Push:askCmds expr result <- hGetLine stdOut - return $ case result of - "sat" -> True - "unsat" -> False + sat <- case result of + "sat" -> do + -- getModel stdIn + -- model <- readModel stdOut + -- putStrLn model + return True + "unsat" -> return False other -> error other + sendCommands [Pop] + return sat where - prog = (T.unpack $ (T.intercalate "\n" (map commandString $ askCmds expr))) ++ "\n" + sendCommands cmds = do + hPutStr stdIn $ (T.unpack (T.intercalate "\n" (map commandString cmds))) ++ "\n" + hFlush stdIn checkSat :: SMTExpr Bool -> IO Bool checkSat expr = do @@ -99,10 +245,13 @@ return result class ToSMTVar a b | a -> b where - toSMTVar :: a -> SMTVar + toSMTVar :: a -> SMTVar b class ToSMT a b where toSMT :: a -> SMTExpr b + +instance ToSMT Int Int where + toSMT = Const instance {-# OVERLAPPABLE #-} (ToSMTVar a b) => ToSMT a b where toSMT :: a -> SMTExpr b diff --git a/src/Language/REST/Types.hs b/src/Language/REST/Types.hs --- a/src/Language/REST/Types.hs +++ b/src/Language/REST/Types.hs @@ -6,6 +6,7 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} +{-# OPTIONS_GHC -Wno-orphans #-} module Language.REST.Types ( prettyPrint @@ -27,7 +28,6 @@ import Language.REST.Op import Language.REST.MetaTerm as MT -import Language.REST.RuntimeTerm as MT data PPArgs = PPArgs { ppReplace :: [(T.Text, T.Text)] @@ -50,14 +50,14 @@ go :: MT.MetaTerm -> T.Text go (MT.Var x) = T.pack x - go t | Just s <- custom t = s + go mt | Just s <- custom mt = s go (MT.RWApp (Op op) [t1, t2]) | Just op' <- L.lookup op infixOps = T.pack $ printf "%s %s %s" (goParens t1) op' (goParens t2) go (MT.RWApp (Op op) []) = op go (MT.RWApp (Op op) xs) = T.concat [op, "(" , T.intercalate ", " (map go xs) , ")"] - goParens t | needsParens t = T.pack $ printf "(%s)" (go t) - goParens t | otherwise = go t + goParens mt | needsParens mt = T.pack $ printf "(%s)" (go mt) + goParens mt | otherwise = go mt needsParens (MT.RWApp (Op op) _) = op `elem` (map fst infixOps) needsParens _ = False diff --git a/src/Language/REST/WQO.hs b/src/Language/REST/WQO.hs deleted file mode 100644 --- a/src/Language/REST/WQO.hs +++ /dev/null @@ -1,329 +0,0 @@ -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE ScopedTypeVariables #-} - -module Language.REST.WQO ( - empty - , insert - , insertMaybe - , orderings - , getRelation - , merge - , mergeAll - , notStrongerThan - , WQO - , QORelation(..) - , ExtendOrderingResult(..) - , relevantTo - , singleton - , null - , getPO - , getECs - , elems) where - -import Prelude hiding (null, EQ, GT) -import GHC.Generics (Generic) -import qualified Data.Map as M -import Control.Monad -import Data.Hashable -import Data.Maybe -import Debug.Trace -import qualified Data.List as L -import qualified Data.Set as S - -import qualified Language.REST.EquivalenceClass as EC -import qualified Language.REST.PartialOrder as PO -import Language.REST.Op -import Language.REST.Types -import Language.REST.SMT - -type PartialOrder = PO.PartialOrder -type EquivalenceClass = EC.EquivalenceClass - -data QORelation = QGT | QEQ deriving (Ord, Eq, Generic, Hashable) - -instance Show QORelation where - show QGT = ">" - show QEQ = "≈" - -instance {-# OVERLAPPING #-} ToSMTVar a Int => ToSMT (WQO a) Bool where - toSMT (WQO ecs po) = And $ ecsSMT ++ posSMT where - - toSMT' :: a -> SMTExpr Int - toSMT' = toSMT - - ecsSMT = do - ec <- S.toList ecs - let ecl = EC.toList ec - guard $ length ecl >= 2 - return $ Equal (map toSMT' ecl) - - posSMT = do - (ec, vars) <- PO.toDescsList po - var <- S.toList vars - return $ Greater (toSMT $ EC.head ec) (toSMT $ EC.head var) - - - -getPO (WQO _ po) = po -getECs (WQO ecs _) = ecs - --- Invariant: the first set contains all ECs -data WQO a = WQO (S.Set (EquivalenceClass a)) (PartialOrder (EquivalenceClass a)) - deriving (Ord, Eq, Generic, Hashable) - -instance (Show a, Eq a, Hashable a) => Show (WQO a) where - show (WQO ecs _) | S.null ecs = "⊤" - show (WQO ecs po) = L.intercalate " ∧ " (map show ecs' ++ po') - where - ecs' = filter (not . EC.isSingleton) $ S.toList ecs - po' = - if PO.isEmpty po - then [] - else [show po] - -- else [show $ PO.mapUnsafe ecHead po] - -- ecHead (x, y) = (EC.head x, EC.head y) - -null :: Eq a => WQO a -> Bool -null wqo = wqo == empty - -empty :: WQO a -empty = WQO S.empty PO.empty - -singleton :: (Ord a, Eq a, Hashable a) => (a, a, QORelation) -> Maybe (WQO a) -singleton t = insertMaybe empty t - -{-# INLINE elems #-} -elems :: (Ord a) => WQO a -> S.Set a -elems (WQO ec _) = S.unions $ map EC.elems (S.toList ec) - -{-# INLINE getEquivalenceClasses #-} -getEquivalenceClasses :: (Ord a, Eq a, Hashable a) => WQO a -> a -> a - -> (Maybe (EquivalenceClass a), Maybe (EquivalenceClass a)) -getEquivalenceClasses (WQO classes _) source target = (t, u) - where - t = L.find (EC.isMember source) classes' - u = L.find (EC.isMember target) classes' - classes' = S.toList classes - -{-# INLINE getEquivalenceClasses' #-} -getEquivalenceClasses' (WQO classes _) source target = - do - t <- L.find (EC.isMember source) classes' - if EC.isMember target t - then return (t, t) - else ((,) t) <$> L.find (EC.isMember target) classes' - where - classes' = S.toList classes - -{-# INLINE getRelation #-} -getRelation :: (Ord a, Eq a, Hashable a) => WQO a -> a -> a -> Maybe QORelation -getRelation _ f g | f == g = Just QEQ -getRelation wqo@(WQO _ po) source target - | Just (s, t) <- getEquivalenceClasses' wqo source target - = if s == t - then Just QEQ - else - if PO.gt po s t - then Just QGT - else Nothing - | otherwise = Nothing - -expandEC :: (Ord a, Eq a, Hashable a) => WQO a -> EquivalenceClass a -> a -> WQO a -expandEC (WQO ecs po) ec x = WQO ecs' po' - where - ec' = EC.insert x ec - ecs' = S.insert ec' $ S.delete ec ecs - po' = PO.replaceUnsafe [ec] ec' po - -mergeECs :: (Ord a, Eq a, Hashable a) => WQO a -> EquivalenceClass a -> EquivalenceClass a -> WQO a -mergeECs (WQO ecs po) ec1 ec2 = WQO ecs' po' - where - ec' = EC.union ec1 ec2 - ecs' = S.insert ec' $ S.delete ec2 $ S.delete ec1 ecs - po' = PO.replaceUnsafe [ec1, ec2] ec' po - -type ECMap a = M.Map (EquivalenceClass a) (EquivalenceClass a) - -{-# SPECIALISE notStrongerThan :: WQO Op -> WQO Op -> Bool #-} -notStrongerThan :: forall a . (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Bool -notStrongerThan w1 w2 | w1 == w2 = True -notStrongerThan (WQO ecs po) (WQO ecs' po') = result where - result = case mkEcsMap M.empty (S.toList ecs) of - Just ecsMap -> all (gt ecsMap) (PO.toDescsList po) - Nothing -> False - - mkEcsMap :: ECMap a -> [EquivalenceClass a] -> Maybe (ECMap a) - mkEcsMap buf [] = Just buf - mkEcsMap buf (ec:rest) = - do - ec' <- L.find (ec `EC.isSubsetOf`) (S.toList ecs') - mkEcsMap (M.insert ec ec' buf) rest - gt ecsMap (ec, descs) = - let - Just ec' = M.lookup ec ecsMap - in - descs `S.isSubsetOf` (PO.descendents ec' po') - - - - -mergeAll :: forall a. (Show a, Ord a, Eq a, Hashable a) => [WQO a] -> Maybe (WQO a) -mergeAll [] = Just empty -mergeAll [x] = Just x -mergeAll (x : x' : xs) = do - y <- merge x x' - mergeAll (y : xs) - -trace' _ x = x - -{-# INLINE merge #-} -merge :: forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Maybe (WQO a) -merge lhs@(WQO ecs po) rhs@(WQO ecs' po') | S.disjoint (elems lhs) (elems rhs) - = Just $ WQO (S.union ecs ecs') (PO.unionDisjointUnsafe po po') -merge lhs rhs | otherwise = - if S.size (elems lhs) >= S.size (elems rhs) - then merge' lhs rhs - else merge' rhs lhs - -{-# SPECIALISE merge' :: WQO Op -> WQO Op -> Maybe (WQO Op) #-} -merge' :: forall a. (Ord a, Eq a, Hashable a) => WQO a -> WQO a -> Maybe (WQO a) -merge' lhs rhs@(WQO ecs po) = trace' message $ result where - - message = "Merge " ++ (show $ hash lhs) ++ " " ++ (show $ hash rhs) - - withEQs' = go lhs ecsFacts - - result = do - withEQs <- withEQs' - go withEQs poFacts - - ecsFacts :: [(a, a, QORelation)] - ecsFacts = concatMap ecFacts (S.toList ecs) - - ecFacts ec = - let - xs = EC.toList ec - in - map (\(a, b) -> (a, b, QEQ)) (zip xs (tail xs)) - - poFacts :: [(a, a, QORelation)] - poFacts = - map (\(a, b) -> (head (EC.toList a), head (EC.toList b), QGT)) (PO.toList po) - - go r [] = Just r - go r (x : xs) = - do - r' <- insertMaybe r x - go r' xs - - -data ExtendOrderingResult a = - ValidExtension (WQO a) - | AlreadyImplied - | Contradicts - -relevantTo :: (Ord a, Eq a, Hashable a) => WQO a -> S.Set a -> S.Set a -> WQO a -relevantTo wqo0 as bs = go empty cartesianProduct where - - cartesianProduct = do - x <- S.toList as - y <- S.toList bs - return (x, y) - - get _ (ValidExtension w) = w - get w AlreadyImplied = w - get _ _ = undefined - - go wqo [] = wqo - go wqo ((f, g) : xs) | f == g = go wqo xs - go wqo ((f, g) : xs) | Just r <- getRelation wqo0 f g - , wqo' <- get wqo $ insert wqo (f, g, r) - = go wqo' xs - go wqo ((f, g) : xs) | Just r <- getRelation wqo0 g f - , wqo' <- get wqo $ insert wqo (g, f, r) - = go wqo' xs - go wqo (_ : xs) | otherwise = go wqo xs - -{-# INLINE insertMaybe #-} -{-# SPECIALISE insertMaybe :: WQO Op -> (Op, Op, QORelation) -> Maybe (WQO Op) #-} -insertMaybe :: (Ord a, Eq a, Hashable a) => WQO a -> (a, a, QORelation) -> Maybe (WQO a) -insertMaybe wqo t = case insert wqo t of - ValidExtension wqo' -> Just wqo' - AlreadyImplied -> Just wqo - Contradicts -> Nothing - - - -{-# SPECIALISE insert :: WQO Op -> (Op, Op, QORelation) -> ExtendOrderingResult Op #-} -insert :: (Ord a, Eq a, Hashable a) => WQO a -> (a, a, QORelation) -> ExtendOrderingResult a -insert _ (f, g, QGT) | f == g = Contradicts -insert wqo (f, g, r) | Just r' <- getRelation wqo f g - = if r == r' then AlreadyImplied else Contradicts -insert wqo (f, g, _) | isJust $ getRelation wqo g f = Contradicts - -insert wqo@(WQO ecs po) (f, g, QEQ) = ValidExtension $ - case getEquivalenceClasses wqo f g of - (Nothing, Nothing) -> - let - ecs' = S.insert (EC.fromList [f, g]) ecs - in - WQO ecs' po - (Just ec, Nothing) -> expandEC wqo ec g - (Nothing, Just ec) -> expandEC wqo ec f - (Just ec1, Just ec2) -> mergeECs wqo ec1 ec2 - -insert wqo@(WQO ecs po) (f, g, QGT) = ValidExtension $ - case getEquivalenceClasses wqo f g of - (Nothing, Nothing) -> - let - f' = EC.singleton f - g' = EC.singleton g - ecs' = S.insert f' $ S.insert g' ecs - Just po' = PO.insert po f' g' - in - WQO ecs' po' - (Just ec, Nothing) -> - let - g' = EC.singleton g - ecs' = S.insert g' ecs - Just po' = PO.insert po ec g' - in - WQO ecs' po' - - (Nothing, Just ec) -> - let - f' = EC.singleton f - ecs' = S.insert f' ecs - Just po' = PO.insert po f' ec - in - WQO ecs' po' - (Just ec1, Just ec2) -> - WQO ecs (PO.insertUnsafe po ec1 ec2) - - -orderings :: forall a. (Ord a, Eq a, Hashable a) => S.Set a -> S.Set (WQO a) -orderings ops = go S.empty (S.singleton empty) where - - insert' w t | ValidExtension w' <- insert w t = Just w' - insert' _ _ = Nothing - - go :: S.Set (WQO a) -> S.Set (WQO a) -> S.Set (WQO a) - go seen acc | S.null acc = seen - go seen acc = - let - ordering = head $ S.toList acc - acc' = S.delete ordering acc - seen' = S.insert ordering seen - newOrderings = - S.fromList $ do - f <- S.toList ops - g <- S.toList (S.delete f ops) - o <- [QEQ, QGT] - maybeToList (insert' ordering (f,g, o)) - newOrderings' = S.difference newOrderings seen - in - go seen' (S.union acc' newOrderings') diff --git a/src/Language/REST/WQOConstraints.hs b/src/Language/REST/WQOConstraints.hs new file mode 100644 --- /dev/null +++ b/src/Language/REST/WQOConstraints.hs @@ -0,0 +1,112 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE FlexibleContexts #-} +module Language.REST.WQOConstraints + ( + WQOConstraints(..) + , ConstraintGen + , liftC + , cmapConstraints + , numOrderings + , isUnsatisfiable + , intersectAll + , unionAll + , intersectRelation + , runStateConstraints + , singleton + ) where + +import Control.Monad.Identity +import Control.Monad.State.Strict +import qualified Data.List as L +import Data.Hashable +import qualified Data.Set as S + +import Prelude hiding (GT, EQ) + +import qualified Language.REST.Internal.WQO as WQO +import Language.REST.Types +import Language.REST.SMT (ToSMTVar) + +type WQO = WQO.WQO + +trace' :: String -> a -> a +trace' _ x = x + +data WQOConstraints impl m = OC + { addConstraint :: forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a + , intersect :: forall a. (Show a, Eq a, Ord a, Hashable a) => impl a -> impl a -> impl a + , isSatisfiable :: forall a. (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => impl a -> m Bool + , notStrongerThan :: forall a. (ToSMTVar a Int, Eq a, Ord a, Hashable a) => impl a -> impl a -> m Bool + , noConstraints :: forall a. (Eq a, Ord a, Hashable a) => impl a + , permits :: forall a. (Show a, Eq a, Ord a, Hashable a) => impl a -> WQO a -> Bool + , relevantConstraints :: forall a. (Eq a, Ord a, Hashable a) => impl a -> S.Set a -> S.Set a -> impl a + , union :: forall a. (Eq a, Ord a, Hashable a) => impl a -> impl a -> impl a + , unsatisfiable :: forall a. impl a + , elems :: forall a. (Eq a, Ord a, Hashable a) => impl a -> S.Set a + , getOrdering :: forall a. impl a -> Maybe (WQO a) + , simplify :: forall a. (Eq a, Ord a, Hashable a) => impl a -> impl a + } + +numOrderings :: (Show a, Ord a, Eq a, Ord a, Hashable a) => S.Set a -> WQOConstraints oc m -> oc a -> Int +numOrderings elems impl oc = S.size $ S.filter (permits impl oc) (WQO.orderings elems) + +isUnsatisfiable :: (Functor m, ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => WQOConstraints oc m -> oc a -> m Bool +isUnsatisfiable OC{isSatisfiable} c = not <$> isSatisfiable c + +singleton :: (Eq a, Ord a, Hashable a) => WQOConstraints oc m -> WQO a -> oc a +singleton OC{addConstraint, noConstraints} c = addConstraint c noConstraints + +intersectAll :: (Eq a, Ord a, Hashable a, Show a, Show (oc a)) => WQOConstraints oc m -> [oc a] -> oc a +intersectAll OC{noConstraints} [] = noConstraints +intersectAll OC{intersect} (x:xs) = L.foldl' go x xs + where + go t1 t2 = trace' ("Intersect " ++ (show t1)) $ intersect t1 t2 + +unionAll :: (Eq a, Ord a, Hashable a, Show a, Show (oc a)) => WQOConstraints oc m -> [oc a] -> oc a +unionAll OC{unsatisfiable} [] = unsatisfiable +unionAll OC{union} (x:xs) = L.foldl' go x xs + where + go t1 t2 = trace' ("Union " ++ (show t1)) $ union t1 t2 + +intersectRelation :: + (Ord a, Eq a, Ord a, Hashable a, Show a) => + WQOConstraints oc m -> oc a -> (a, a, Relation) -> oc a +intersectRelation oc impl (f, g, r) = + case nc r of + Just impl' -> intersect oc impl impl' + Nothing -> unsatisfiable oc + where + nc GT = fmap (singleton oc) (WQO.singleton (f, g, WQO.QGT)) + nc EQ = fmap (singleton oc) (WQO.singleton (f, g, WQO.QEQ)) + nc GTE = do + wqo1 <- WQO.singleton (f, g, WQO.QGT) + wqo2 <- WQO.singleton (f, g, WQO.QEQ) + return $ union oc (singleton oc wqo1) (singleton oc wqo2) + + + +-- ConstraintGen impl R >= t u returns the constraints on >= that guarantee +-- the resulting relation >=', we have: +-- 1. x >= y implies x >=' y +-- 2. t lift(R(>=')) u +-- Where R generates { == , >=, > } from the underlying ordering +-- R is used to enable optimizations + +type ConstraintGen oc base lifted m = + forall m' . (WQOConstraints oc m' -> Relation -> oc base -> lifted -> lifted -> m (oc base)) + +cmapConstraints :: (lifted' -> lifted) -> ConstraintGen oc base lifted m -> ConstraintGen oc base lifted' m +cmapConstraints f cgen impl r oc t u = cgen impl r oc (f t) (f u) + +liftC :: (m Bool -> m' Bool) -> WQOConstraints impl m -> WQOConstraints impl m' +liftC f oc = oc{ + isSatisfiable = isSatisfiable' + , notStrongerThan = notStrongerThan' + } + where + isSatisfiable' c1 = f (isSatisfiable oc c1) + notStrongerThan' c1 c2 = f (notStrongerThan oc c1 c2) + +runStateConstraints :: ConstraintGen oc base lifted (State a) -> a -> ConstraintGen oc base lifted Identity +runStateConstraints cgen initState impl r oc t u = Identity $ evalState (cgen impl r oc t u) initState diff --git a/src/Language/REST/WQOConstraints/ADT.hs b/src/Language/REST/WQOConstraints/ADT.hs new file mode 100644 --- /dev/null +++ b/src/Language/REST/WQOConstraints/ADT.hs @@ -0,0 +1,266 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE CPP #-} + +#define OPTIMIZE_WQO + +module Language.REST.WQOConstraints.ADT where + +import GHC.Generics (Generic) + +import Debug.Trace +import Data.Hashable +import Control.Monad.State.Lazy +import qualified Data.Set as S +import qualified Data.Maybe as Mb +import qualified Data.Map.Strict as M +import qualified Language.REST.Internal.WQO as WQO +import qualified Language.REST.WQOConstraints as OC +import Language.REST.SMT +import Language.REST.Op +import System.IO (Handle) +import Text.Printf + +type WQO = WQO.WQO + +data ConstraintsADT a = + Sat (WQO a) + | Unsat + | Union (ConstraintsADT a) (ConstraintsADT a) + | Intersect (ConstraintsADT a) (ConstraintsADT a) + deriving (Eq, Ord, Generic, Hashable) + +instance {-# OVERLAPPING #-} (ToSMTVar a Int) => ToSMT (ConstraintsADT a) Bool where + toSMT (Sat w) = toSMT w + toSMT Unsat = smtFalse + toSMT (Union w1 w2) = Or [toSMT w1, toSMT w2] + toSMT (Intersect w1 w2) = And [toSMT w1, toSMT w2] + +{-# SPECIALIZE cost :: ConstraintsADT Op -> Int #-} +cost :: (Ord a, Eq a, Hashable a) => ConstraintsADT a -> Int +cost (Union lhs rhs) = min (cost lhs) (cost rhs) +cost (Intersect lhs rhs) = cost lhs + cost rhs +cost (Sat wqo) = S.size $ WQO.elems wqo +cost Unsat = 100 + +minDepth :: ConstraintsADT a -> Int +minDepth (Union lhs rhs) = 1 + min (minDepth lhs) (minDepth rhs) +minDepth (Intersect lhs rhs) = 1 + min (minDepth lhs) (minDepth rhs) +minDepth _ = 1 + +maxDepth :: ConstraintsADT a -> Int +maxDepth (Union lhs rhs) = 1 + max (maxDepth lhs) (maxDepth rhs) +maxDepth (Intersect lhs rhs) = 1 + max (maxDepth lhs) (maxDepth rhs) +maxDepth _ = 1 + +intersect :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a + +#ifdef OPTIMIZE_WQO +-- Optimization +intersect (Sat t) (Sat u) = + case WQO.merge t u of + Just t' -> Sat t' + Nothing -> Unsat +#endif + +intersect (Sat w) v | w == WQO.empty = v +intersect v (Sat w) | w == WQO.empty = v +intersect _ Unsat = Unsat +intersect Unsat _ = Unsat +intersect t1 t2 | t1 == t2 = t1 +intersect t1 (Union t2 t3) | t1 == t2 || t1 == t3 = t1 +#ifdef OPTIMIZE_WQO +intersect (Sat w1) (Intersect (Sat w2) t2) = + case WQO.merge w1 w2 of + Just w' -> intersect (Sat w') t2 + Nothing -> Unsat +intersect (Sat w1) (Intersect t2 (Sat w2)) = + case WQO.merge w1 w2 of + Just w' -> intersect (Sat w') t2 + Nothing -> Unsat +intersect (Intersect t1 (Sat w1)) (Sat w2) = + case WQO.merge w1 w2 of + Just w' -> intersect t1 (Sat w') + Nothing -> Unsat +intersect (Intersect (Sat w1) t1) (Sat w2) = + case WQO.merge w1 w2 of + Just w' -> intersect t1 (Sat w') + Nothing -> Unsat +#endif +intersect t1 t2 = Intersect t1 t2 + +union :: Eq a => ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a +union (Sat w) _ | w == WQO.empty = Sat w +union _ (Sat w) | w == WQO.empty = Sat w +union (Intersect a b) c | a == c || b == c = c +union a (Intersect b c) | a == b || a == c = a +union a (Union b c) | a == b = union a c +union Unsat s = s +union s Unsat = s +union c1 c2 | c1 == c2 = c1 +union c1 c2 = Union c1 c2 + +addConstraint + :: (Ord a, Hashable a) => WQO a -> ConstraintsADT a -> ConstraintsADT a +addConstraint o c = intersect (Sat o) c + +relevantConstraints + :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> S.Set a -> S.Set a -> ConstraintsADT a +relevantConstraints c _ _ = c + +notStrongerThan + :: (Eq a, ToSMTVar a Int) + => ConstraintsADT a + -> ConstraintsADT a + -> SMTExpr Bool +notStrongerThan t1 t2 | t1 == t2 = smtTrue +notStrongerThan t1 _ | t1 == noConstraints = smtTrue +notStrongerThan t1 t2 | otherwise = Implies (toSMT t2) (toSMT t1) + +noConstraints :: ConstraintsADT a +noConstraints = Sat (WQO.empty) + +unsatisfiable :: ConstraintsADT a +unsatisfiable = Unsat + +trace' :: String -> a -> a +trace' = trace + +{-# SPECIALIZE getConstraints :: ConstraintsADT Op -> [WQO Op] #-} +getConstraints :: forall a. (Show a, Ord a, Hashable a) => ConstraintsADT a -> [WQO a] +getConstraints adt = -- trace' ("Get constraints, size : " ++ (show $ dnfSize adt)) $ + evalState (getConstraints' adt) (GCState M.empty M.empty) + +data GCState a = GCState { + cs :: M.Map (ConstraintsADT a) (GCResult a) + , ms :: M.Map (WQO a, WQO a) (Maybe (WQO a)) +} + +type GCResult a = [WQO a] + +type GCMonad a = State (GCState a) (GCResult a) + +cached :: (Ord a) => ConstraintsADT a -> GCMonad a -> GCMonad a +cached key thunk = do + cache <- gets cs + case M.lookup key cache of + Just result -> trace'' ("ADT Cache hit") $ return result + Nothing -> trace'' ("ADT Cache miss") $ do + result <- trace'' "Do thunk" thunk + trace'' "Done" $ modify (\st -> st{cs = M.insert key result (cs st)}) + return result + where + trace'' _ x = x + -- trace' = trace + +cached' :: (Hashable a, Show a, Ord a) => (WQO a, WQO a) -> Maybe (WQO a) -> State (GCState a) (Maybe (WQO a)) +cached' (lhs, rhs) thunk = do + cache <- gets ms + case M.lookup (lhs, rhs) cache of + Just result -> trace'' ("WQO Cache hit") $ return result + Nothing -> trace'' ("WQO Cache miss" ++ show (lhs, rhs)) $ do + trace'' "Done" $ modify (\st -> st{ms = M.insert (rhs, lhs) thunk $ M.insert (lhs, rhs) thunk (ms st)}) + return thunk + where + trace'' _ x = x + -- trace' = trace + +getConstraints' :: forall a. (Show a, Ord a, Hashable a) => ConstraintsADT a -> State (GCState a) [WQO a] +getConstraints' (Sat w) = return [w] +getConstraints' Unsat = return [] +getConstraints' c@(Union lhs rhs) = + cached c $ do + c1' <- cached c1 $ getConstraints' c1 + c2' <- cached c2 $ getConstraints' c2 + return $ c1' ++ c2' + where + (c1, c2) = + if cost lhs < cost rhs + then (lhs, rhs) + else (rhs, lhs) +getConstraints' c@(Intersect lhs rhs) = cached c $ do + c1' <- cached c1 $ getConstraints' c1 + if null c1' + then return [] + else (cached c2 $ getConstraints' c2) >>= go c1' + where + go :: [WQO a] -> [WQO a] -> State (GCState a) [WQO a] + go c1' c2' = flatten <$> + (sequence $ do + wqo1 <- c1' + wqo2 <- c2' + return (cached' (wqo1, wqo2) $ WQO.merge wqo1 wqo2)) + flatten = concatMap Mb.maybeToList + (c1, c2) = + if cost lhs > cost rhs + then (lhs, rhs) + else (rhs, lhs) + +dnfSize :: ConstraintsADT a -> Int +dnfSize (Sat _w) = 1 +dnfSize Unsat = 0 +dnfSize (Union w1 w2) = dnfSize w1 + dnfSize w2 +dnfSize (Intersect w1 w2) = dnfSize w1 * dnfSize w2 + +-- toDNF (Union lhs rhs) = S.union (toDNF lhs) (toDNF rhs) +-- toDNF (Intersect lhs rhs) = +-- let +-- ldnf = toDNF lhs +-- rdnf = toDNF rhs +-- in +-- S.unions + +simplify :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> ConstraintsADT a +simplify _adt = undefined +-- simplify adt = case getConstraints adt of +-- [] -> Unsat +-- (x:xs) -> foldl go (Sat x) xs +-- where +-- go a x = Union (Sat x) a + +permits + :: (Ord a, Hashable a, Show a) + => ConstraintsADT a + -> WQO.WQO a + -> Bool +permits adt wqo = any (`WQO.notStrongerThan` wqo) (getConstraints adt) + +isSatisfiable :: (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => ConstraintsADT a -> SMTExpr Bool +isSatisfiable s = toSMT s + -- trace (show (minDepth s) ++ " " ++ show (maxDepth s)) $ not $ null $ getConstraints s + +instance (Eq a, Hashable a, Show a) => Show (ConstraintsADT a) where + -- show s = go 0 s where + -- go n (Sat w) = indent n $ show w + -- go n Unsat = indent n $ "⊥" + -- go n (Union w t ) = indent n $ printf "∪\n%s\n%s" (go (n+1) w) (go (n+1) t) + -- go n (Intersect w t) = indent n $ printf "∩\n%s\n%s" (go (n+1) w) (go (n+1) t) + + -- indent 0 s = s + -- indent n s = take (n - 1) (repeat '|') ++ '+':s + + show (Sat w) = show w + show Unsat = "⊥" + show (Union w t ) = printf "(%s ∨\n %s)" (show w) (show t) + show (Intersect w t) = printf "(%s ∧ %s)" (show w) (show t) + +adtOC :: (Handle, Handle) -> OC.WQOConstraints ConstraintsADT IO +adtOC z3 = OC.liftC (checkSat' z3) adtOC' + +adtOC' :: OC.WQOConstraints ConstraintsADT SMTExpr +adtOC' = OC.OC + addConstraint + intersect + isSatisfiable + notStrongerThan + noConstraints + permits + relevantConstraints + union + unsatisfiable + undefined + undefined + simplify diff --git a/src/Language/REST/WQOConstraints/Lazy.hs b/src/Language/REST/WQOConstraints/Lazy.hs new file mode 100644 --- /dev/null +++ b/src/Language/REST/WQOConstraints/Lazy.hs @@ -0,0 +1,130 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Language.REST.WQOConstraints.Lazy ( + lazyOC + , addConstraint + , intersect + , isSatisfiable + , noConstraints + , singleton + , union + , unsatisfiable + , LazyOC + ) where + +import Text.Printf +import GHC.Generics (Generic) +import Data.Hashable +import qualified Data.Set as S + +import qualified Language.REST.Internal.WQO as WQO +import qualified Language.REST.WQOConstraints as OC +import qualified Language.REST.WQOConstraints.ADT as ADT + +type WQO = WQO.WQO + +-- Partially lazy ordering constraints: +-- thunks computation after showing satisfiability + +type Thunk a = ADT.ConstraintsADT a + +data LazyOC a = + Unsat + | Sat (WQO a) (Thunk a) + deriving (Eq, Ord, Generic, Hashable) + +getOrdering :: LazyOC a -> Maybe (WQO a) +getOrdering (Sat wqo _) = Just wqo +getOrdering _ = Nothing + +eval :: (Eq a, Ord a, Hashable a) => ADT.ConstraintsADT a -> LazyOC a +eval (ADT.Sat w) = Sat w ADT.Unsat +eval ADT.Unsat = Unsat +eval (ADT.Union lhs rhs) = + case eval t1 of + Sat w t1' -> Sat w (ADT.union t1' t2) + Unsat -> eval t2 + where + (t1, t2) = (lhs, rhs) + -- if ADT.minDepth lhs < ADT.minDepth rhs + -- then (lhs, rhs) + -- else (rhs, lhs) + +eval (ADT.Intersect t1 t2) = + case (eval t1, eval t2) of + (Sat c1 t1', Sat c2 t2') -> + let + rest = + (ADT.intersect (ADT.Sat c1) t2') `ADT.union` + (ADT.intersect (ADT.Sat c2) t1') `ADT.union` + (ADT.intersect t1' t2') + in + case WQO.merge c1 c2 of + Just c' -> Sat c' rest + Nothing -> eval rest + _ -> Unsat + + +toADT :: Eq a => LazyOC a -> ADT.ConstraintsADT a +toADT Unsat = ADT.Unsat +toADT (Sat w r) = ADT.union (ADT.Sat w) r + +instance (Show a, Eq a, Ord a, Hashable a) => Show (LazyOC a) where + show Unsat = "⊥" + show (Sat s r) = printf "%s ∨ lazy(%s)" (show s) (show r) + +noConstraints :: LazyOC a +noConstraints = Sat (WQO.empty) ADT.Unsat + +unsatisfiable :: LazyOC a +unsatisfiable = Unsat + +union :: Eq a => LazyOC a -> LazyOC a -> LazyOC a +union Unsat s = s +union s Unsat = s +union (Sat s _) _ | s == WQO.empty = noConstraints +union _ (Sat s _) | s == WQO.empty = noConstraints +union (Sat s1 r1) (Sat s2 r2) = Sat s1 (ADT.union (ADT.Sat s2) (ADT.union r1 r2)) + +intersect :: (Ord a, Hashable a) => LazyOC a -> LazyOC a -> LazyOC a +intersect t1 t2 = eval $ ADT.intersect (toADT t1) (toADT t2) + +isSatisfiable :: LazyOC a -> Bool +isSatisfiable (Sat _ _) = True +isSatisfiable Unsat = False + +singleton :: WQO a -> LazyOC a +singleton c = Sat c ADT.Unsat + +relevantConstraints + :: (Eq a, Ord a, Hashable a) => LazyOC a -> S.Set a -> S.Set a -> LazyOC a +relevantConstraints c _ _ = c + +notStrongerThan :: (Monad m, Eq a) => LazyOC a -> LazyOC a -> m Bool +notStrongerThan _ Unsat = return True +notStrongerThan t1 t2 = return $ t1 == t2 + +addConstraint :: (Ord a, Hashable a) => ADT.WQO a -> LazyOC a -> LazyOC a +addConstraint o c = eval $ ADT.addConstraint o (toADT c) + +permits :: (Ord a, Hashable a) => LazyOC a -> WQO.WQO a -> Bool +permits Unsat _ = False +permits (Sat s1 thunk) wqo = s1 `WQO.notStrongerThan` wqo || permits (eval thunk) wqo + +lazyOC :: Monad m => OC.WQOConstraints LazyOC m +lazyOC = OC.OC + addConstraint + intersect + (return . isSatisfiable) + notStrongerThan + noConstraints + permits + relevantConstraints + union + unsatisfiable + undefined + getOrdering + id diff --git a/src/Language/REST/WQOConstraints/Strict.hs b/src/Language/REST/WQOConstraints/Strict.hs new file mode 100644 --- /dev/null +++ b/src/Language/REST/WQOConstraints/Strict.hs @@ -0,0 +1,152 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Language.REST.WQOConstraints.Strict ( + strictOC + , strictOC' + , addConstraint + , difference + , getOrdering + , intersect + , isSatisfiable + , isUnsatisfiable + , noConstraints + , notStrongerThan + , permits + , relevantConstraints + , union + , unsatisfiable + , singleton + , StrictOC + , elems + ) where + +import Control.Monad.Identity +import GHC.Generics (Generic) +import Data.Hashable +import Data.Maybe +import qualified Data.List as L +import qualified Data.Set as S + +import qualified Language.REST.WQOConstraints as OC +import qualified Language.REST.Internal.WQO as WQO + +type WQO = WQO.WQO + +-- Represents a set of constraints on a WQO on type `a` + +-- The constraints are represented as a set ws of WQOs +-- The constraints permit any WQO w that is a valid extension of some (w' in wqos) + + +data StrictOC a = StrictOC (S.Set (WQO a)) + deriving (Eq, Ord, Generic, Hashable) + +instance (Show a, Eq a, Ord a, Hashable a) => Show (StrictOC a) where + show (StrictOC cs) | S.null cs = "unsatisfiable" + show (StrictOC cs) | S.member WQO.empty cs = "no constraints" + show (StrictOC cs) = L.intercalate " ∨ \n" (map show (S.toList cs)) + -- where + -- show' o@(OpOrdering s) = if S.size s > 1 then printf "(%s)" (show o) else show o + +getOrdering :: StrictOC a -> Maybe (WQO a) +getOrdering (StrictOC o) = + listToMaybe (S.toList o) + +elems :: Ord a => StrictOC a -> S.Set a +elems (StrictOC sets) = S.unions $ map WQO.elems (S.toList sets) + +noConstraints :: forall a. (Eq a, Ord a, Hashable a) => StrictOC a +noConstraints = StrictOC (S.singleton (WQO.empty)) + +unsatisfiable :: StrictOC a +unsatisfiable = StrictOC S.empty + +isUnsatisfiable :: Eq a => StrictOC a -> Bool +isUnsatisfiable c = c == unsatisfiable + +isSatisfiable :: Eq a => StrictOC a -> Bool +isSatisfiable c = c /= unsatisfiable + +notStrongerThan :: forall m a. (Monad m, Eq a, Ord a, Hashable a) => StrictOC a -> StrictOC a -> m Bool +notStrongerThan (StrictOC _lhs) (StrictOC _rhs) = return False + +-- The difference of two constraints `a` and `b` is new constraints such that +-- intersect (diff a b) b = a +difference :: (Eq a, Ord a, Hashable a) => StrictOC a -> StrictOC a -> StrictOC a +difference (StrictOC lhs) (StrictOC rhs) = + StrictOC (S.difference lhs rhs) + +-- The union of two constraints `a` and `b` is new constraints that only +-- permits an ordering if permitted by either `a` or `b` +union :: (Eq a, Ord a, Hashable a) => StrictOC a -> StrictOC a -> StrictOC a +union (StrictOC lhs) (StrictOC rhs) = + fromSet $ S.union lhs rhs + +fromSet :: (Eq a, Ord a, Hashable a) => S.Set (WQO a) -> StrictOC a +fromSet oc = -- StrictOC oc + StrictOC $ go [] (L.sortOn (length . WQO.elems) $ S.toList oc) + where + go include [] = S.fromList include + go include (x : xs) = + if any (`WQO.notStrongerThan` x) (include ++ xs) + then go include xs + else go (x : include) xs + + +-- The intersection of two constraints `a` and `b` is new constraints that only +-- permits the orderings permitted by both `a` and `b` +intersect :: (Show a, Eq a, Ord a, Hashable a) => StrictOC a -> StrictOC a -> StrictOC a +intersect (StrictOC lhs) (StrictOC rhs) = result + -- trace (printf "%s intersect %s yields %s" (show lhs) (show rhs) (show result)) result + where + result = fromSet $ S.fromList $ + do + lhs' <- S.toList lhs + rhs' <- S.toList rhs + maybeToList (WQO.merge lhs' rhs') + +addConstraint :: (Eq a, Ord a, Hashable a) => WQO a -> StrictOC a -> StrictOC a +addConstraint c (StrictOC oc) = StrictOC $ S.fromList $ do + c' <- S.toList oc + maybeToList $ WQO.merge c c' + +singleton :: (Eq a, Ord a, Hashable a) => WQO a -> StrictOC a +singleton c = addConstraint c noConstraints + +relevantConstraints :: forall a. (Eq a, Ord a, Hashable a) => StrictOC a -> S.Set a -> S.Set a -> StrictOC a +relevantConstraints (StrictOC oc0) as bs = go (S.toList oc0) unsatisfiable + where + go :: [WQO a] -> StrictOC a -> StrictOC a + go [] oc = oc + go (o : rest) exist = + let + o' = WQO.relevantTo o as bs + in + if WQO.null o' + then noConstraints + else go rest (union (singleton o) exist) + +permits :: (Eq a, Ord a, Hashable a) => StrictOC a -> WQO a -> Bool +permits (StrictOC permitted) desired = + any (`WQO.notStrongerThan` desired) (S.toList permitted) + +strictOC :: Monad m => OC.WQOConstraints StrictOC m +strictOC = OC.OC + addConstraint + intersect + (return . isSatisfiable) + notStrongerThan + noConstraints + permits + relevantConstraints + union + unsatisfiable + elems + getOrdering + id + +strictOC' :: OC.WQOConstraints StrictOC Identity +strictOC' = strictOC diff --git a/src/Language/REST/WorkStrategy.hs b/src/Language/REST/WorkStrategy.hs deleted file mode 100644 --- a/src/Language/REST/WorkStrategy.hs +++ /dev/null @@ -1,37 +0,0 @@ -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -module Language.REST.WorkStrategy where - -import Language.REST.ExploredTerms as ET -import Language.REST.Path -import Language.REST.Rewrite - -import Data.Hashable -import qualified Data.List as L - -type GetWork m rule term et oc = [Path rule term oc] -> (term -> et) -> ExploredTerms et oc m -> (Path rule term oc, [Path rule term oc]) - -newtype WorkStrategy rule term et oc = WorkStrategy (forall m . GetWork m rule term et oc) - -bfs = WorkStrategy bfs' - -notVisitedFirst :: (Eq term, Eq rule, Eq oc, Eq et, Hashable et) => WorkStrategy rule term et oc -notVisitedFirst = WorkStrategy notVisitedFirst' - -bfs' :: [Path rule term oc] -> (term -> et) -> ExploredTerms et oc m -> (Path rule term oc, [Path rule term oc]) -bfs' (h:t) _ _ = (h, t) - -notVisitedFirst' :: (Eq term, Eq rule, Eq oc, Eq et, Hashable et) => GetWork m rule term et oc -notVisitedFirst' paths toET et = - case L.find (\p -> not (ET.visited (toET $ runtimeTerm p) et)) paths of - Just p -> (p, L.delete p paths) - Nothing -> (head paths, tail paths) - -commutesLast :: forall term oc et . (Eq term, Eq oc, Eq et, Hashable et) => WorkStrategy Rewrite term et oc -commutesLast = WorkStrategy go where - go paths toET et = - case L.find (\p -> not (ET.visited (toET $ runtimeTerm p) et || fromComm p)) paths of - Just p -> (p, L.delete p paths) - Nothing -> (head paths, tail paths) - fromComm ([], _) = False - fromComm (steps, _) = (getName . rule . last) steps == Just "mpComm" diff --git a/src/Lists.hs b/src/Lists.hs deleted file mode 100644 --- a/src/Lists.hs +++ /dev/null @@ -1,34 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -module Lists where - -import Prelude hiding (reverse) - -import Language.REST.Op -import Language.REST.Core -import Language.REST.Types -import qualified Language.REST.MetaTerm as MT -import DSL - -import qualified Data.HashSet as S - -xs = MT.Var "xs" -ys = MT.Var "ys" - -nil = MT.RWApp "nil" [] -(.:) t1 t2 = MT.RWApp "cons" [t1, t2] -reverse t = MT.RWApp "reverse" [t] -(.++) lhs rhs = MT.RWApp "append" [lhs, rhs] - - -evalRWs = S.fromList [ - reverse (x .: xs) ~> reverse xs .++ (x .: nil) - , reverse nil ~> nil - , nil .++ xs ~> xs - , (x .: xs) .++ ys ~> x .: (xs .++ ys) - , reverse (reverse (MT.RWApp "xs" [])) ~> MT.RWApp "xs" [] - ] - -userRWs = S.fromList [ - reverse (xs .++ ys) ~> (reverse ys) .++ (reverse xs) - , (reverse ys) .++ (reverse xs) ~> reverse (xs .++ ys) - ] diff --git a/src/Main.hs b/src/Main.hs deleted file mode 100644 --- a/src/Main.hs +++ /dev/null @@ -1,151 +0,0 @@ -{-# LANGUAGE ImplicitParams #-} -{-# LANGUAGE OverloadedStrings #-} - -module Main where - -import Control.Monad.IO.Class -import Control.Monad.Identity -import Data.Time.Clock -import Data.Hashable -import qualified Data.HashSet as S -import qualified Data.HashMap.Strict as M -import qualified Data.Maybe as Mb -import Debug.Trace -import Data.List (intercalate) -import Control.Monad -import Data.Bifunctor (bimap) -import Text.Printf - -import qualified Arith as A -import qualified Compiler as C -import qualified Group as G -import BagExample -import WQODot as WQODot -import Language.REST.RESTDot -import Language.REST.Dot -import DSL -import Nat -import qualified Set as Set -import qualified Multiset as MS -import NonTerm as NT -import qualified Lists as Li - -import Language.REST.MultisetOrder (possibilities) -import Language.REST.ConcreteOC -import Language.REST.Core -import Language.REST.AbstractOC -import Language.REST.OCToAbstract -import Language.REST.Op -import Language.REST.OpOrdering -import Language.REST.OrderingConstraints as OC -import qualified Language.REST.OrderingConstraints.Strict as SC -import qualified Language.REST.OrderingConstraints.Lazy as LC -import qualified Language.REST.OrderingConstraints.ADT as AC -import Language.REST.RPO -import Language.REST.WQO as WQO -import Language.REST.WorkStrategy -import Language.REST.Path -import Language.REST.ProofGen -import Language.REST.Rest -import Language.REST.Types -import Language.REST.SMT -import qualified Language.REST.MetaTerm as MT -import Language.REST.RuntimeTerm as RT -import Language.REST.Rewrite - - -data ConsType = Strict | Lazy | ADT - -mkArithRESTGraph gt ct = mkRESTGraph gt ct A.evalRWs A.userRWs -mkCompilerRESTGraph gt ct = mkRESTGraph gt ct C.evalRWs C.userRWs -mkGroupRESTGraph gt ct = mkRESTGraph gt ct G.evalRWs G.userRWs -mkListsRESTGraph gt ct = mkRESTGraph gt ct Li.evalRWs Li.userRWs -mkSetsRESTGraph gt ct = mkRESTGraph gt ct Set.evalRWs Set.userRWs -mkNonTermRestGraph gt ct = mkRESTGraph gt ct NT.evalRWs NT.userRWs -mkMSRESTGraph gt ct = mkRESTGraph gt ct MS.evalRWs MS.userRWs - - -explain z3 (t, u) = printf "%s ≥ %s requires:\n%s\n\n\n" (show t) (show u) (show $ rpoGTE t u) - where - ?impl = AC.adtOC z3 - -explainOrient :: [String] -> IO () -explainOrient ts0 = withZ3 go where - go z3 = - let - ts = map parseTerm ts0 - pairs = zip ts (tail ts) - in - do - mapM_ (explain z3) pairs - printf "Result:\n%s\n" (show $ orient ts) - (isSatisfiable (AC.adtOC z3) (orient ts)) >>= print - where - ?impl = lift (AC.adtOC z3) rpo - -mkRESTGraph :: (MonadIO m, Hashable (c Op), Ord (c Op), Show (c Op)) => - GraphType - -> (SolverHandle -> OrderingConstraints c m) - -> S.HashSet Rewrite - -> S.HashSet Rewrite - -> String - -> String - -> String - -> m () -mkRESTGraph gt oc evalRWs userRWs name term target = - -- mkRESTGraph' gt (fuelOC 5) evalRWs userRWs name term target - withZ3 $ \z3 -> mkRESTGraph' gt (lift (oc z3) rpo) evalRWs userRWs name term target - -mkRESTGraph' :: (MonadIO m, Show c, Hashable c, Ord c) => - GraphType - -> AbstractOC c RuntimeTerm m - -> S.HashSet Rewrite - -> S.HashSet Rewrite - -> String - -> String - -> String - -> m () -mkRESTGraph' gt impl evalRWs userRWs name term target = - do - let pr (Rewrite t u _) = printf "%s → %s" (pp t) (pp u) - liftIO $ mapM_ (\rw -> putStrLn $ pr rw) $ S.toList userRWs - liftIO $ mapM_ (\rw -> putStrLn $ pr rw) $ S.toList evalRWs - start <- liftIO $ getCurrentTime - (PathsResult paths, targetPath) <- rest - RESTParams - { re = evalRWs - , ru = userRWs - , toET = id - , target = if target == "" then Nothing else (Just (parseTerm target)) - , workStrategy = notVisitedFirst - , ocImpl = impl - , initRes = pathsResult - } (parseTerm term) - end <- liftIO $ getCurrentTime - liftIO $ printf "REST run completed, in %s\n" $ show $ diffUTCTime end start - liftIO $ putStrLn "Drawing graph" - -- let prettyPrinter = PrettyPrinter pr pp show - let prettyPrinter = PrettyPrinter pr pp (const "") True - liftIO $ writeDot name gt prettyPrinter (toOrderedSet paths) - liftIO $ when (target /= "") - (case targetPath of - Just tp -> printf "FOUND TARGET. Proof:\n%s\n" (toProof tp) - Nothing -> printf "TARGET %s NOT FOUND\n" (pp (parseTerm target))) - - - -lhs :: RuntimeTerm -lhs = "ite(isNull(ys), null, reverse(tail(ys)) + cons(head(ys),null)) + (reverse(tail(ds)) + cons(head(ds), null))" - -rhs :: RuntimeTerm -rhs = "(ite(isNull(ys), null, reverse(tail(ys)) + cons(head(ys), null)) + reverse(tail(ds))) + cons(head(ds), null)" - -mkWQOGraph :: String -> String -> IO () -mkWQOGraph name wqoS = mkWQOGraph' name wqo where - Just wqo = parseOO wqoS - -mkWQOGraph' :: (Ord a, Hashable a, Show a) => String -> WQO.WQO a -> IO () -mkWQOGraph' name wqo = mkGraph name (WQODot.toDigraph wqo) - -main :: IO () -main = return () diff --git a/src/Multiset.hs b/src/Multiset.hs deleted file mode 100644 --- a/src/Multiset.hs +++ /dev/null @@ -1,44 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -module Multiset where - -import Data.Text () -import DSL -import Language.REST.MetaTerm -import Language.REST.Op -import Language.REST.Rewrite -import qualified Data.HashSet as S -import Prelude hiding (singleton) - -x \/ y = RWApp "union" [x, y] - -singleton x = RWApp "m" [x] -cons x y = RWApp "cons" [x, y] -multisetOf x = RWApp "toMS" [x] -ite a b c = RWApp "ite" [a,b,c] -hd x = RWApp "head" [x] -tl x = RWApp "tail" [x] -isEmpty x = RWApp "isEmpty" [x] -empty = RWApp "empty" [] - -xs = RWApp "xs" [] -ys = RWApp "ys" [] - -expandM xs = multisetOf xs ~> ite (isEmpty xs) empty (singleton (hd xs) \/ multisetOf (tl xs)) - -userRWs = S.fromList $ - [ - commutes (\/) `named` "mpComm" - , assocL (\/) `named` "mpAssoc" - , assocR (\/) `named` "mpAssoc" - , (singleton x) \/ (multisetOf y) ~> multisetOf (cons x y) - ] - -evalRWs = S.fromList - [ multisetOf (cons x y) ~> (singleton x) \/ (multisetOf y) - , expandM xs - , expandM ys - ] - -perm1s = "union(m(y), union(toMS(cons(a,xs)),toMS(ys)))" -perm1t = "union(m(a), union(toMS(xs), toMS(cons(y,ys))))" diff --git a/src/MultisetOrdering.hs b/src/MultisetOrdering.hs deleted file mode 100644 --- a/src/MultisetOrdering.hs +++ /dev/null @@ -1,141 +0,0 @@ -{-# LANGUAGE ScopedTypeVariables#-} -module MultisetOrdering where - -import Data.Hashable -import Language.REST.Dot hiding (toGraph) -import qualified Data.Maybe as Mb -import qualified Data.List as L -import qualified Language.REST.MultiSet as M -import qualified Data.HashMap.Strict as Mp -import qualified Data.HashSet as S -import Language.REST.Types - -data Replace a = - ReplaceOne a a - | Replace a [a] - deriving (Show) - -data MultisetGE a = MultisetGE [Replace a] deriving (Show) - -type GTE a = a -> a -> Bool - -type Indexed a = (a, Int) - -type IndexedMultisetPair a = (Indexed (M.MultiSet (Indexed a)) , Indexed (M.MultiSet (Indexed a))) - -multisetGE :: forall a . Eq a => GTE a -> M.MultiSet a -> M.MultiSet a -> Maybe (MultisetGE a) -multisetGE gte ts0 us0 = go [] (M.toList ts0) (M.toList us0) - where - equiv t u = t `gte` u && u `gte` t - gt t u = t `gte` u && not (u `gte` t) - - go :: [Replace a] -> [a] -> [a] -> Maybe (MultisetGE a) - go rs (t : ts) us | Just u <- L.find (equiv t) us - = go ((ReplaceOne t u):rs) ts (L.delete u us) - - go rs (t : ts) us | otherwise = - let - (lts, us') = L.partition (t `gt`) us - in - go ((Replace t lts) : rs) ts us' - go rs ts [] = Just $ MultisetGE $ (map ((flip Replace) []) ts) ++ rs - go _ [] _ = Nothing - - -multisetOrd :: (Eq a, Hashable a, Ord a) => [a] -> [a] -> Maybe (MultisetGE a) -multisetOrd ts us = multisetGE (>=) (M.fromList ts) (M.fromList us) - -zindex :: [a] -> [(a, Int)] -zindex xs = zip xs [0 ..] - -indexMS :: (Eq a, Hashable a) => M.MultiSet a -> M.MultiSet (a, Int) -indexMS ms = M.fromList $ zindex (M.toList ms) - -mkEdge t u = Edge t u " " "black" " " "solid" - -botNodeName tIndex mIndex = "bot_" ++ show tIndex ++ "_" ++ show mIndex - -botNode tIndex mIndex = - Node (botNodeName tIndex mIndex) "⊥" "solid" "black" - -toGraph' :: forall a. (Eq a, Hashable a, Show a) => GTE a -> [M.MultiSet a] -> DiGraph -toGraph' gte mss = DiGraph "msograph" (toOrderedSet (S.union elemNodes botNodes)) (toOrderedSet edges) - where - indexed :: [(M.MultiSet (a, Int), Int)] - indexed = zindex (map indexMS mss) - - pairs :: [((M.MultiSet (a, Int), Int), (M.MultiSet (a, Int), Int))] - pairs = zip indexed (tail indexed) - - elemNodes = S.fromList $ filter hasEdge $ concatMap toNodes indexed - - hasEdge node = any (`pointsTo` node) $ S.toList edges - - pointsTo edge node = - from edge == nodeID node || to edge == nodeID node - - edges :: S.HashSet Edge - edges = S.fromList $ topEdges ++ (map snd $ replEdges pairs) - - topEdges = map go (M.toList (fst $ head indexed)) where - go (_, index) = - mkEdge "⊤" (nodeName (index, 0)) - - botNodes = S.fromList $ concatMap Mb.maybeToList $ map fst $ replEdges pairs - - nodeName :: (Int, Int) -> String - nodeName (elemIndex, msIndex) = - "n" ++ show elemIndex ++ "_" ++ show msIndex - - replEdges = toEdges Mp.empty - - toEdges :: Mp.HashMap (Int, Int) (Int, Int) -> [IndexedMultisetPair a] -> ([(Maybe Node, Edge)]) - toEdges _ [] = [] - toEdges mp (((ts, tsIndex), (us, usIndex)) : mss) = - concatMap redges repls ++ toEdges mp' mss - where - Just (MultisetGE repls) = multisetGE (\t u -> gte (fst t) (fst u)) ts us - - lookup :: Int -> (Int, Int) - lookup tindex = case Mp.lookup (tindex, tsIndex) mp of - Just t -> t - Nothing -> (tindex, tsIndex) - - mp' = go mp repls where - go mpi [] = mpi - go mpi ((ReplaceOne (_, i) (_, j)):repls') - = go (Mp.insert (j, usIndex) (lookup i) mpi) repls' - go mpi (_:repls') = go mpi repls' - - - redges (Replace (_, index) []) - = [ ( Just (botNode index tsIndex) - , mkEdge - (nodeName (lookup index)) - (botNodeName index tsIndex) - ) ] - redges (ReplaceOne _ _) = [] - redges (Replace (_, tindex) us') = map go us' where - go (_, uindex) = - (Nothing, mkEdge (nodeName (lookup tindex)) (nodeName (uindex, usIndex))) - - toNodes (ms, index) = map go (M.toList ms) where - - go (elem, elemIndex) = - Node - (nodeName (elemIndex, index)) - (show elem) - "solid" - "black" - -toGraph :: (Ord a, Eq a, Hashable a, Show a) => [[a]] -> DiGraph -toGraph mss = toGraph' (>=) $ map M.fromList mss - -mkMSOGraph :: (Ord a, Eq a, Hashable a, Show a) => String -> [[a]] -> IO () -mkMSOGraph name mss = mkGraph name (toGraph mss) - -mkMSOGraphs :: (Ord a, Eq a, Hashable a, Show a) => String -> [[a]] -> IO () -mkMSOGraphs name mss0 = mapM_ go (drop 1 $ L.inits mss0) where - go mss = mkGraph (name ++ show (length mss)) (toGraph mss) - -multisetGE' ts us = multisetGE (>=) (M.fromList ts) (M.fromList us) diff --git a/src/Nat.hs b/src/Nat.hs deleted file mode 100644 --- a/src/Nat.hs +++ /dev/null @@ -1,99 +0,0 @@ -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE OverloadedStrings #-} - -module Nat (termToInt, intToTerm, parseTerm, pp, s, z) where - - -import Data.Text -import Text.ParserCombinators.Parsec.Char -import Text.ParserCombinators.Parsec -import Text.Printf -import Data.String -import qualified Data.List as L - -import qualified Language.REST.MetaTerm as MT -import Language.REST.Op -import Language.REST.Types -import Language.REST.RuntimeTerm as RT -import Language.REST.Types - -s = Op "s" -z = Op "z" - -intToTerm :: Int -> RuntimeTerm -intToTerm 0 = App z [] -intToTerm n = App s [intToTerm (n - 1)] - -termToInt :: (MT.ToMetaTerm a) => a -> Maybe Int -termToInt t = go (MT.toMetaTerm t) where - go (MT.RWApp op []) | op == z = Just 0 - go (MT.RWApp op [t1]) | op == s = (1 +) <$> go t1 - go _ = Nothing - -instance ToRuntimeTerm Int where - toRuntimeTerm = intToTerm - -pp :: MT.ToMetaTerm a => a -> String -pp = prettyPrint (PPArgs [] - [ ("+", "+") - , ("*", "*") - , ("∪", "∪") - , ("union", "∪") - , ("intersect", "∩") - ] showInt) - where - showInt :: MT.MetaTerm -> Maybe Text - showInt t = fmap (pack . show) $ termToInt t - -op :: GenParser Char st Op -op = fmap (Op . pack) (many (alphaNum <|> char '\'')) - -parens p = do - _ <- char '(' - r <- p - _ <- char ')' - return r - -term = try infixTerm <|> nonInfixTerm - where - - nonInfixTerm = try (parens term) <|> try appTerm <|> try numberTerm <|> nullTerm - - numberTerm = do - d1 <- digit - n <- many digit - return $ intToTerm (read (d1 : n)) - - infixOp = - try (string "+") - <|> (try (string "\\/") >> return "∪") - <|> string "*" - - infixTerm = do - t1 <- nonInfixTerm - _ <- spaces - op <- infixOp - _ <- spaces - t2 <- nonInfixTerm - return $ App (Op (pack op)) [t1, t2] - - nullTerm = do - o <- op - return $ App o [] - - appTerm = do - o <- op - trms <- parens $ sepBy1 term (char ',' >> spaces) - return $ App o trms - - -parseTerm :: String -> RuntimeTerm -parseTerm str = - case parse term "" str of - Left err -> error (show err) - Right t -> t - -instance IsString RuntimeTerm where - fromString = parseTerm diff --git a/src/NonTerm.hs b/src/NonTerm.hs deleted file mode 100644 --- a/src/NonTerm.hs +++ /dev/null @@ -1,29 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -module NonTerm where - -import Arith as A -import Data.Text -import DSL -import Nat -import Language.REST.Op -import Language.REST.MetaTerm -import Language.REST.Rewrite -import qualified Data.HashSet as S - -a' x = RWApp (Op "a") [x] -b' x = RWApp (Op "b") [x] -c' x = RWApp (Op "c") [x] -d' x = RWApp (Op "d") [x] - -userRWs :: S.HashSet Rewrite -userRWs = S.fromList $ - [ - a' (b' x) ~> a' (d' x) - , d' (b' x) ~> b' (d' x) - , b' (d' x) ~> d' (b' x) - , d' (b' x) ~> b' (b' (b' x)) - ] - - -evalRWs = A.evalRWs diff --git a/src/Set.hs b/src/Set.hs deleted file mode 100644 --- a/src/Set.hs +++ /dev/null @@ -1,53 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -module Set where - -import Arith as A -import Data.Text -import DSL -import Language.REST.MetaTerm -import Language.REST.Op - -import qualified Data.HashSet as S - -emptyset = RWApp "∅" [] - -x /\ y = RWApp "intersect" [x, y] -x \/ y = RWApp "union" [x, y] - -s0 = RWApp "s₀" [] -s1 = RWApp "s₁" [] - -isSubset t1 t2 = t1 \/ t2 ~> t2 - -userRWs = S.union A.evalRWs $ S.fromList $ - [ - distribL (/\) (\/) - , distribR (/\) (\/) - , distribL (\/) (/\) - , distribR (\/) (/\) - -- assocL (\/) - -- , assocL (/\) - , x /\ x ~> x - , x \/ x ~> x - , x \/ emptyset ~> x - -- , commutes (\/) - -- , commutes (/\) - - -- Example 1 - , s1 /\ s0 ~> emptyset - - -- Example 2 - -- , s0 \/ s1 ~> s0 - ] - -evalRWs = S.union A.userRWs $ S.fromList -- - [ RWApp "t2" [] ~> emptyset - , isSubset (RWApp "right1" []) (RWApp "right" []) - ] - -disjointExample = "union(union(left, right1), union(left,right))" -disjointExample2 = "union(left, union(right1, union(left,right)))" - -example1 = "f(intersect(union(s₀,s₁), s₀))" -example2 = "f(union(intersect(s₀,s₁), s₀))" diff --git a/src/WQODot.hs b/src/WQODot.hs deleted file mode 100644 --- a/src/WQODot.hs +++ /dev/null @@ -1,21 +0,0 @@ -module WQODot where - -import Data.Hashable -import qualified Data.Set as S - -import Language.REST.Dot -import Language.REST.PartialOrder -import Language.REST.WQO - -toDigraph :: (Ord a, Hashable a, Show a) => WQO a -> DiGraph -toDigraph wqo = digraph where - - digraph = DiGraph "wqo" nodes edges - - labelFor ec = 'n' : show (abs $ hash ec) - - nodes = S.map toNode (getECs wqo) - edges = S.fromList $ map toEdge (toList $ getPO wqo) - - toNode ec = Node (labelFor ec) (show ec) "solid" "black" - toEdge (ec1, ec2) = Edge (labelFor ec1) (labelFor ec2) "" "black" "" "solid" diff --git a/test/BagExample.hs b/test/BagExample.hs new file mode 100644 --- /dev/null +++ b/test/BagExample.hs @@ -0,0 +1,118 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeSynonymInstances #-} + +module BagExample (mkBagGraph) where + +import Prelude hiding (EQ, GT) + + +import Control.Monad.Identity +import Language.REST.Dot +import Language.REST.ExploredTerms +import Language.REST.RESTDot +import Language.REST.OCToAbstract +import Language.REST.RewriteRule +import qualified Language.REST.Internal.MultiSet as M +import Language.REST.Internal.MultisetOrder +import Language.REST.Rest +import Language.REST.WQOConstraints as OC +import Language.REST.WQOConstraints.Strict as SC +import Language.REST.Internal.WorkStrategy +import Language.REST.Types +import Language.REST.SMT hiding (GTE) + +import qualified Data.List as L +import qualified Data.HashSet as S +import qualified Data.Text as T +import GHC.Generics (Generic) +import Data.Hashable + +data PChar = PChar Char deriving (Eq, Ord, Generic, Hashable) + +instance ToSMTVar PChar Int where + toSMTVar c = SMTVar $ T.pack $ "char_" ++ show c + +instance Show PChar where + show (PChar c) = return c + +data Bag = Bag String + deriving (Eq, Ord, Generic, Hashable) + +instance Show Bag where + show = showBag + + +toMultiset :: Bag -> M.MultiSet PChar +toMultiset (Bag str) = M.fromList $ map PChar str + + +bag :: String -> Bag +bag = Bag + +data Rewrite = Rewrite Bag (S.HashSet Bag) + deriving (Eq, Ord, Generic, Hashable) + +infixr 1 ~> +(~>) :: String -> [String] -> [String] +(~>) = (:) + +instance RewriteRule IO Rewrite Bag where + apply bag1 (Rewrite bag' result) | bag1 == bag' = return result + apply _ _ | otherwise = return S.empty + + +fromPath :: [String] -> S.HashSet Rewrite +fromPath [] = S.empty +fromPath xs = S.fromList $ map go (zip xs (tail xs)) + where + go :: (String, String) -> Rewrite + go (x, y) = Rewrite (bag x) (S.singleton $ bag y) + + +fromPaths :: [[String]] -> S.HashSet Rewrite +fromPaths paths = S.unions $ map fromPath paths + +start :: String +start = "AAB" + +rules :: S.HashSet Rewrite +rules = fromPaths $ + [ start ~> "ACD" ~> "AAAA" ~> "ABDD" ~> [] + , start ~> "ABD" ~> "AB" ~> "BBD" ~> [] + ] + +showBag :: Bag -> String +showBag (Bag bag1) = "{ " ++ (L.intercalate ", " $ map return bag1) ++ " }" + +showRule :: Rewrite -> String +showRule _ = "" + + +compareChar :: ConstraintGen impl PChar PChar Identity +compareChar impl GTE oc c1 c2 | c1 /= c2 = compareChar impl GT oc c1 c2 +compareChar impl EQ _ c1 c2 | c1 /= c2 = return $ OC.unsatisfiable impl +compareChar impl r oc c1 c2 = return $ intersectRelation impl oc (c1, c2, r) + + +mkBagGraph :: IO () +mkBagGraph = + do + (PathsResult paths, _) <- rest + RESTParams + { re = S.empty + , ru = rules + , toET = id + , target = Nothing + , workStrategy = bfs + , ocImpl = impl + , initRes = pathsResult + , etStrategy = ExploreWhenNeeded + } (bag start) + let prettyPrinter = PrettyPrinter showRule showBag show True + writeDot "example" Tree prettyPrinter (toOrderedSet paths) + where + impl = lift SC.strictOC $ cmapConstraints toMultiset (multisetOrder compareChar) diff --git a/test/Compiler.hs b/test/Compiler.hs new file mode 100644 --- /dev/null +++ b/test/Compiler.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Compiler where + +import qualified Arith as A +import DSL +import Language.REST.Internal.Rewrite (Rewrite) +import Language.REST.MetaTerm +import Language.REST.Op + +import qualified Data.HashSet as S +import Prelude hiding (repeat, seq) + +repeat :: MetaTerm -> MetaTerm -> MetaTerm +repeat n op = RWApp (Op "repeat") [n, op] + +seq :: MetaTerm -> MetaTerm -> MetaTerm +seq op1 op2 = RWApp (Op "seq") [op1, op2] + +nop :: MetaTerm +nop = RWApp (Op "nop") [] + +userRWs :: S.HashSet Rewrite +userRWs = + S.union A.userRWs + (S.fromList $ [ + seq x nop ~> x + , seq nop x ~> x + , repeat zero' x ~> nop + ] ++ (repeat (suc' y) x <~> seq x (repeat y x)) + -- ++ (repeat (suc' y) x <~> seq (repeat y x) x) + ++ (repeat (suc' (suc' zero')) x <~> seq x x)) + +evalRWs :: S.HashSet Rewrite +evalRWs = S.empty -- S.fromList [ ] diff --git a/test/Group.hs b/test/Group.hs new file mode 100644 --- /dev/null +++ b/test/Group.hs @@ -0,0 +1,26 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Group where + +import DSL +import Language.REST.Internal.Rewrite (Rewrite) +import Language.REST.Op +import Language.REST.MetaTerm + +import qualified Data.HashSet as S + +neg :: MetaTerm -> MetaTerm +neg x1 = RWApp (Op "neg") [x1] + +evalRWs :: S.HashSet Rewrite +evalRWs = S.empty + +userRWs :: S.HashSet Rewrite +userRWs = + S.fromList + [ + x #+ zero' ~> x + , zero' #+ x ~> x + , (neg x) #+ x ~> zero' + , (x #+ y) #+ v ~> x #+ (y #+ v) + ] diff --git a/test/KBO.hs b/test/KBO.hs new file mode 100644 --- /dev/null +++ b/test/KBO.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE OverloadedStrings #-} + +module KBO where + +import Language.REST.OCAlgebra +import Language.REST.KBO +import Language.REST.SMT +import Language.REST.RuntimeTerm +import Nat () -- IsString RuntimeTerm + +tests :: SolverHandle -> [(String, IO Bool)] +tests solver = testList where + + gte :: RuntimeTerm -> RuntimeTerm -> IO Bool + gte t u = isSat (kbo solver) (kboGTE t u) + + testList = + [ ("Comm" , gte "f(a, b)" "f(b, a)") + , ("Assoc" , gte "f(a, f(b, c))" "f((a b), c)") + , ("Dist" , not <$> gte "f(a, g(b, c))" "g(f(a, b), f(a, c))") + ] diff --git a/test/LazyOC.hs b/test/LazyOC.hs new file mode 100644 --- /dev/null +++ b/test/LazyOC.hs @@ -0,0 +1,16 @@ +module LazyOC where + +import Data.Maybe +import Language.REST.WQOConstraints.Lazy as LC +import Language.REST.Internal.OpOrdering + +oo :: String -> OpOrdering +oo = fromJust . parseOO + +tests :: [(String, Bool)] +tests = [ + ("intersect", + not $ LC.isSatisfiable $ LC.addConstraint (oo "g > f") + (LC.addConstraint (oo "f > g ^ f > s") LC.noConstraints) + ) + ] diff --git a/test/Lists.hs b/test/Lists.hs new file mode 100644 --- /dev/null +++ b/test/Lists.hs @@ -0,0 +1,40 @@ +{-# LANGUAGE OverloadedStrings #-} +module Lists where + +import Prelude hiding (reverse) + +import Language.REST.Internal.Rewrite (Rewrite) +import qualified Language.REST.MetaTerm as MT +import DSL hiding (t1, t2) + +import qualified Data.HashSet as S + +xs, ys, nil :: MT.MetaTerm +xs = MT.Var "xs" +ys = MT.Var "ys" +nil = MT.RWApp "nil" [] + +(.:) :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm +(.:) t1 t2 = MT.RWApp "cons" [t1, t2] + +reverse :: MT.MetaTerm -> MT.MetaTerm +reverse t = MT.RWApp "reverse" [t] + +(.++) :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm +(.++) lhs rhs = MT.RWApp "append" [lhs, rhs] + + +evalRWs :: S.HashSet Rewrite +evalRWs = S.fromList [ + reverse (x .: xs) ~> reverse xs .++ (x .: nil) + , reverse nil ~> nil + , nil .++ xs ~> xs + , (x .: xs) .++ ys ~> x .: (xs .++ ys) + , reverse (reverse (MT.RWApp "xs" [])) ~> MT.RWApp "xs" [] + ] + +userRWs :: S.HashSet Rewrite +userRWs = S.fromList [ + reverse (xs .++ ys) ~> (reverse ys) .++ (reverse xs) + , (reverse ys) .++ (reverse xs) ~> reverse (xs .++ ys) + ] diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,183 @@ +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} + +module Main where + +import Control.Monad.IO.Class +import Control.Monad.Identity +import Data.Time.Clock +import Data.Hashable +import qualified Data.HashSet as S +import Text.Printf + +import qualified Arith as A +import qualified Compiler as C +import qualified Group as G +import Language.REST.RESTDot +import Language.REST.Dot +import Language.REST.Internal.WorkStrategy +import DSL +import Nat +import Set as Set +import qualified Multiset as MS +import NonTerm as NT +import qualified Lists as Li + +import Language.REST.Core +import Language.REST.ExploredTerms +import Language.REST.OCAlgebra +import Language.REST.OCToAbstract +import Language.REST.Op +import Language.REST.WQOConstraints as OC +import qualified Language.REST.WQOConstraints.Strict as SC +import qualified Language.REST.WQOConstraints.ADT as AC +import Language.REST.KBO (kbo) +import Language.REST.LPO (lpo, lpoStrict) +import Language.REST.RPO +import Language.REST.ProofGen +import Language.REST.Rest +import Language.REST.Types +import Language.REST.SMT +import Language.REST.RuntimeTerm as RT +import Language.REST.Internal.Rewrite + + +data ConsType = Strict | Lazy | ADT + +mkArithRESTGraph, + mkCompilerRESTGraph, + mkGroupRESTGraph, + mkListsRESTGraph, + mkSetsRESTGraph, + mkNonTermRestGraph, + mkMSRESTGraph + :: SolverType -> String -> String -> GraphParams -> IO () +mkArithRESTGraph ct = mkRESTGraph ct A.evalRWs A.userRWs +mkCompilerRESTGraph ct = mkRESTGraph ct C.evalRWs C.userRWs +mkGroupRESTGraph ct = mkRESTGraph ct G.evalRWs G.userRWs +mkListsRESTGraph ct = mkRESTGraph ct Li.evalRWs Li.userRWs +mkSetsRESTGraph ct = mkRESTGraph ct Set.evalRWs Set.userRWs +mkNonTermRestGraph ct = mkRESTGraph ct NT.evalRWs NT.userRWs +mkMSRESTGraph ct = mkRESTGraph ct MS.evalRWs MS.userRWs + +explain :: (Show t2, Show t3, Show a) => (t2 -> t3 -> a) -> (t2, t3) -> IO () +explain f0 (t, u) = printf "%s ≥ %s requires:\n%s\n\n\n" (show t) (show u) (show $ f0 t u) + +explainOrient :: [String] -> IO () +explainOrient ts0 = withZ3 go where + go :: SolverHandle -> IO () + go _z3 = + let + ts = map parseTerm ts0 + pairs = zip ts (tail ts) + in + do + mapM_ (explain (refine impl (top impl))) pairs + printf "Result:\n%s\n" (show $ orient impl ts) + (isSatisfiable SC.strictOC (orient impl ts)) >>= print + where + impl :: OCAlgebra (SC.StrictOC Op) RuntimeTerm Identity + impl = lift SC.strictOC lpo + +data GraphParams = GraphParams + { gShowConstraints :: Bool + , gTarget :: Maybe String + , gGraphType :: GraphType + , gShowRejects :: Bool + , gUseETOpt :: Bool + } + +defaultParams :: GraphParams +defaultParams = GraphParams False Nothing Tree True True + +withTarget :: String -> GraphParams -> GraphParams +withTarget target0 gp = gp{gTarget = Just target0} + +withShowConstraints :: GraphParams -> GraphParams +withShowConstraints gp = gp{gShowConstraints = True} + +withNoETOpt :: GraphParams -> GraphParams +withNoETOpt gp = gp{gUseETOpt = False} + +withHideRejects :: GraphParams -> GraphParams +withHideRejects gp = gp{gShowRejects = False} + +data SolverType = LPOStrict | LPO | RPO | KBO | Fuel Int + +mkRESTGraph :: + SolverType + -> S.HashSet Rewrite + -> S.HashSet Rewrite + -> String + -> String + -> GraphParams + -> IO () +mkRESTGraph LPOStrict evalRWs0 userRWs0 name term0 params = + withZ3 $ \z3 -> mkRESTGraph' (lift (AC.adtOC z3) lpoStrict) evalRWs0 userRWs0 name term0 params +mkRESTGraph LPO evalRWs0 userRWs0 name term0 params = + withZ3 $ \z3 -> mkRESTGraph' (lift (AC.adtOC z3) lpo) evalRWs0 userRWs0 name term0 params +mkRESTGraph RPO evalRWs0 userRWs0 name term0 params = + withZ3 $ \z3 -> mkRESTGraph' (lift (AC.adtOC z3) rpo) evalRWs0 userRWs0 name term0 params +mkRESTGraph KBO evalRWs0 userRWs0 name term0 params = + withZ3 $ \z3 -> mkRESTGraph' (kbo z3) evalRWs0 userRWs0 name term0 params +mkRESTGraph (Fuel n) evalRWs0 userRWs0 name term0 params = + mkRESTGraph' (fuelOC n) evalRWs0 userRWs0 name term0 params + +mkRESTGraph' :: (MonadIO m, Show c, Hashable c, Ord c) => + OCAlgebra c RuntimeTerm m + -> S.HashSet Rewrite + -> S.HashSet Rewrite + -> String + -> String + -> GraphParams + -> m () +mkRESTGraph' impl evalRWs0 userRWs0 name term0 params = + do + let pr (Rewrite t u _) = printf "%s → %s" (pp t) (pp u) + liftIO $ mapM_ (\rw -> putStrLn $ pr rw) $ S.toList userRWs0 + liftIO $ mapM_ (\rw -> putStrLn $ pr rw) $ S.toList evalRWs0 + start <- liftIO $ getCurrentTime + (PathsResult paths, targetPath) <- rest + RESTParams + { re = evalRWs0 + , ru = userRWs0 + , toET = id + , target = fmap parseTerm (gTarget params) + , workStrategy = bfs + , ocImpl = impl + , initRes = pathsResult + , etStrategy = if gUseETOpt params then ExploreWhenNeeded else ExploreAlways + } (parseTerm term0) + end <- liftIO $ getCurrentTime + liftIO $ printf "REST run completed, in %s\n" $ show $ diffUTCTime end start + liftIO $ putStrLn "Drawing graph" + let showCons = if gShowConstraints params then show else const "" + let prettyPrinter = PrettyPrinter pr pp showCons (gShowRejects params) + liftIO $ writeDot name (gGraphType params) prettyPrinter (toOrderedSet paths) + liftIO $ case gTarget params of + Just target1 -> + (case targetPath of + Just tp -> printf "FOUND TARGET. Proof:\n%s\n" (toProof tp) + Nothing -> printf "TARGET %s NOT FOUND\n" (pp (parseTerm target1))) + Nothing -> return () + +challengeRulesNoCommute :: S.HashSet Rewrite +challengeRulesNoCommute = S.fromList + [ x /\ x ~> x + , x \/ x ~> x + , x \/ emptyset ~> x + , x /\ emptyset ~> emptyset + , distribL (/\) (\/) + , distribR (/\) (\/) + , distribL (\/) (/\) + , distribR (\/) (/\) + , assocL (\/) + , assocR (\/) + ] + +main :: IO () +main = do + mkRESTGraph RPO S.empty (S.insert (s1 /\ s0 ~> emptyset) challengeRulesNoCommute) "fig4" "f(intersect(union(s₀,s₁), s₀))" (withNoETOpt defaultParams) + mkRESTGraph RPO S.empty (S.fromList $ [x #+ y ~> y #+ x] ++ ((x #+ y) #+ v <~> x #+ (y #+ v))) "fig8-noopt" "a + (b + a)" (withNoETOpt defaultParams) + mkRESTGraph RPO S.empty (S.fromList $ [x #+ y ~> y #+ x] ++ ((x #+ y) #+ v <~> x #+ (y #+ v))) "fig8-opt" "a + (b + a)" defaultParams diff --git a/test/Multiset.hs b/test/Multiset.hs new file mode 100644 --- /dev/null +++ b/test/Multiset.hs @@ -0,0 +1,57 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Multiset where + +import Data.Text () +import DSL hiding (a, b, c) +import Language.REST.MetaTerm +import Language.REST.Internal.Rewrite +import qualified Data.HashSet as S + +(\/) :: MetaTerm -> MetaTerm -> MetaTerm +x1 \/ y1 = RWApp "union" [x1, y1] + +singleton, multisetOf :: MetaTerm -> MetaTerm +singleton x1 = RWApp "m" [x1] +multisetOf x1 = RWApp "toMS" [x1] + +cons :: MetaTerm -> MetaTerm -> MetaTerm +cons x1 y1 = RWApp "cons" [x1, y1] + +ite :: MetaTerm -> MetaTerm -> MetaTerm -> MetaTerm +ite a b c = RWApp "ite" [a,b,c] + +hd, tl, isEmpty :: MetaTerm -> MetaTerm +hd x1 = RWApp "head" [x1] +tl x1 = RWApp "tail" [x1] +isEmpty x1 = RWApp "isEmpty" [x1] + +empty :: MetaTerm +empty = RWApp "empty" [] + +xs, ys :: MetaTerm +xs = RWApp "xs" [] +ys = RWApp "ys" [] + +expandM :: MetaTerm -> Rewrite +expandM xs0 = multisetOf xs0 ~> ite (isEmpty xs0) empty (singleton (hd xs0) \/ multisetOf (tl xs0)) + +userRWs :: S.HashSet Rewrite +userRWs = S.fromList $ + [ + commutes (\/) `named` "mpComm" + , assocL (\/) `named` "mpAssoc" + , assocR (\/) `named` "mpAssoc" + , (singleton x) \/ (multisetOf y) ~> multisetOf (cons x y) + ] + +evalRWs :: S.HashSet Rewrite +evalRWs = S.fromList + [ multisetOf (cons x y) ~> (singleton x) \/ (multisetOf y) + , expandM xs + , expandM ys + ] + +perm1t, perm1s :: String +perm1s = "union(m(y), union(toMS(cons(a,xs)),toMS(ys)))" +perm1t = "union(m(a), union(toMS(xs), toMS(cons(y,ys))))" diff --git a/test/MultisetOrder.hs b/test/MultisetOrder.hs --- a/test/MultisetOrder.hs +++ b/test/MultisetOrder.hs @@ -4,21 +4,23 @@ import Control.Monad.Identity -import Debug.Trace (trace) -import Language.REST.MultiSet as M -import Language.REST.MultisetOrder -import Language.REST.OrderingConstraints.Strict as SC -import Language.REST.OrderingConstraints as OC +import Language.REST.Internal.MultiSet as M +import Language.REST.Internal.MultisetOrder +import Language.REST.WQOConstraints.Strict as SC +import Language.REST.WQOConstraints as OC import Language.REST.Types compareChar :: ConstraintGen impl Char Char Identity compareChar impl r oc c1 c2 = Identity $ intersectRelation impl oc (c1, c2, r) +existingOC :: StrictOC Char existingOC = OC.intersectRelation strictOC' SC.noConstraints ('a', 'c', GTE) +ms :: StrictOC Char -> MultiSet Char -> MultiSet Char -> Identity (StrictOC Char) ms = multisetOrder compareChar strictOC' GTE +multisetNext :: Identity (StrictOC Char) multisetNext = ms existingOC (M.fromList "bac") (M.fromList "aaaa") unsat :: Identity (StrictOC Char) diff --git a/test/NonTerm.hs b/test/NonTerm.hs new file mode 100644 --- /dev/null +++ b/test/NonTerm.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE OverloadedStrings #-} + +module NonTerm where + +import Arith as A +import DSL +import Language.REST.Op +import Language.REST.MetaTerm +import Language.REST.Internal.Rewrite +import qualified Data.HashSet as S + +a', b', c', d' :: MetaTerm -> MetaTerm +a' x1 = RWApp (Op "a") [x1] +b' x1 = RWApp (Op "b") [x1] +c' x1 = RWApp (Op "c") [x1] +d' x1 = RWApp (Op "d") [x1] + +userRWs :: S.HashSet Rewrite +userRWs = S.fromList $ + [ + a' (b' x) ~> a' (d' x) + , d' (b' x) ~> b' (d' x) + , b' (d' x) ~> d' (b' x) + , d' (b' x) ~> b' (b' (b' x)) + ] + +evalRWs :: S.HashSet Rewrite +evalRWs = A.evalRWs diff --git a/test/OpOrdering.hs b/test/OpOrdering.hs --- a/test/OpOrdering.hs +++ b/test/OpOrdering.hs @@ -2,11 +2,11 @@ module OpOrdering where -import Language.REST.Op -import Language.REST.OpOrdering -import Language.REST.WQO +import Language.REST.Internal.OpOrdering +import Language.REST.Internal.WQO import Data.Maybe as Mb +tests :: [(String, Bool)] tests = [ ("parse", fromJust ( diff --git a/test/QuickCheckTests.hs b/test/QuickCheckTests.hs --- a/test/QuickCheckTests.hs +++ b/test/QuickCheckTests.hs @@ -1,32 +1,30 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE OverloadedStrings #-} +{-# OPTIONS_GHC -Wno-orphans #-} module QuickCheckTests where import Test.QuickCheck import Test.QuickCheck.Monadic import Control.Monad.Identity +import Data.Hashable (Hashable) import Data.Maybe as Mb import qualified Data.Text as T -import Debug.Trace (trace) -import Language.REST.Core hiding (syms) -import qualified Language.REST.PartialOrder as PO -import qualified Language.REST.WQO as WQO -import qualified Language.REST.OrderingConstraints as OC -import qualified Language.REST.OrderingConstraints.Strict as SC -import qualified Language.REST.OrderingConstraints.Lazy as LC +import Language.REST.Internal.OpOrdering (OpOrdering) +import qualified Language.REST.Internal.PartialOrder as PO +import qualified Language.REST.Internal.WQO as WQO +import qualified Language.REST.WQOConstraints as OC +import qualified Language.REST.WQOConstraints.Strict as SC +import qualified Language.REST.WQOConstraints.Lazy as LC import Language.REST.RPO -import Nat import Language.REST.Op -import Language.REST.Types import Language.REST.RuntimeTerm import Prelude hiding (EQ, GT) -import Text.Printf - type WQO = WQO.WQO +syms :: [(T.Text, Int)] syms = [ ("f", 3) , ("g", 2) @@ -104,18 +102,29 @@ instance Arbitrary (WQO Op) where arbitrary = gen_wqo +prop_poTrans :: Op -> Op -> Op -> PO.PartialOrder Op -> Property prop_poTrans f g h po = PO.gt po f g && PO.gt po g h ==> PO.gt po f h - where - types = f::Op -prop_wqoTrans f g h wqo = f `gte` g && g `gte` h ==> f `gte` h +prop_wqoTrans :: Op -> Op -> Op -> WQO.WQO Op -> Property +prop_wqoTrans f0 g0 h wqo = f0 `gte` g0 && g0 `gte` h ==> f0 `gte` h where gte f g = Mb.isJust $ WQO.getRelation wqo f g - types = f::Op +prop_rpoTrans + :: RuntimeTerm + -> RuntimeTerm + -> RuntimeTerm + -> OpOrdering + -> Property prop_rpoTrans t u v wqo = synGTE wqo t u && synGTE wqo u v ==> synGTE wqo t v +prop_rpoCons + :: (?impl::OC.WQOConstraints impl m, Hashable (impl Op), Eq (impl Op), Show (impl Op)) + => OC.WQOConstraints impl IO + -> RuntimeTerm + -> RuntimeTerm + -> Property prop_rpoCons impl t u = monadicIO $ do isSat <- run $ OC.isSatisfiable impl constraints pre isSat @@ -124,6 +133,7 @@ constraints = rpoGTE t u ordering = Mb.fromJust (OC.getOrdering impl constraints) +prop_permits :: [(Op, Op, WQO.QORelation)] -> Bool prop_permits steps = SC.permits (SC.noConstraints) (toWQO steps) -- Should fail @@ -138,6 +148,7 @@ -- where -- types = t0::RuntimeTerm +tests :: IO [()] tests = sequence [ -- quickCheckWith stdArgs{maxDiscardRatio = 1000} prop_rpot2 diff --git a/test/RPO.hs b/test/RPO.hs --- a/test/RPO.hs +++ b/test/RPO.hs @@ -3,47 +3,56 @@ module RPO where -import Debug.Trace -import Control.Monad.Identity import Data.Hashable -import DSL import Nat import Language.REST.Op -import Language.REST.OpOrdering as OpOrdering -import Language.REST.OrderingConstraints as OC +import Language.REST.Internal.OpOrdering as OpOrdering +import Language.REST.WQOConstraints as OC import Language.REST.RuntimeTerm import Language.REST.RPO -import Language.REST.WQO +import Language.REST.Internal.WQO import Data.Maybe as Mb +bigLeft, bigRight :: RuntimeTerm bigLeft = "f(h(s(g(z,nil))),f(g(z,z),nil,h(z)),f(z,nil,z) + g(z,s(z)))" bigRight = "g(g(g(s(nil),z),s(z) + z),g(s(s(h(nil))),s(z)))" +massiveLeft :: RuntimeTerm massiveLeft = "concat(ite(isLeaf(la1Bz), cons(LeaflqdcselectLeaf1(la1Bz), nil), concat(flatten(NodelqdcselectNode1(la1Bz)), flatten(NodelqdcselectNode2(la1Bz)))), concat(ite(isLeaf(ra1BA), cons(LeaflqdcselectLeaf1(ra1BA), nil), concat(flatten(NodelqdcselectNode1(ra1BA)), flatten(NodelqdcselectNode2(ra1BA)))), nsa1By))" +massiveRight :: RuntimeTerm massiveRight = "concat(ite(isLeaf(la1Bz), cons(LeaflqdcselectLeaf1(la1Bz), nil), concat(flatten(NodelqdcselectNode1(la1Bz)), flatten(NodelqdcselectNode2(la1Bz)))), ite(isnil(ite(isLeaf(ra1BA), cons(LeaflqdcselectLeaf1(ra1BA), nil), concat(flatten(NodelqdcselectNode1(ra1BA)), flatten(NodelqdcselectNode2(ra1BA))))), nsa1By, cons(lqdcselectcons1(ite(isLeaf(ra1BA), cons(LeaflqdcselectLeaf1(ra1BA), nil), concat(flatten(NodelqdcselectNode1(ra1BA)), flatten(NodelqdcselectNode2(ra1BA))))), concat(lqdcselectcons2(ite(isLeaf(ra1BA), cons(LeaflqdcselectLeaf1(ra1BA), nil), concat(flatten(NodelqdcselectNode1(ra1BA)), flatten(NodelqdcselectNode2(ra1BA))))), nsa1By))))" +listsLeft :: RuntimeTerm listsLeft = "concat(ite(isNil(ysaLe), Nil, concat(reverse(lqdcselectcons2(ysaLe)), cons(lqdcselectcons1(ysaLe), Nil))), concat(reverse(lqdcselectcons2(dsdOz)), cons(lqdcselectcons1(dsdOz), Nil)))" +listsRight :: RuntimeTerm listsRight = "concat(concat(ite(isNil(ysaLe), Nil, concat(reverse(lqdcselectcons2(ysaLe)), cons(lqdcselectcons1(ysaLe), Nil))), reverse(lqdcselectcons2(dsdOz))), cons(lqdcselectcons1(dsdOz), Nil))" +flattenLeft2 :: RuntimeTerm flattenLeft2 = "concat(ite(isLeaf(la1Bz), cons(LeaflqdcselectLeaf1(la1Bz), nil), concat(flatten(NodelqdcselectNode1(la1Bz)), flatten(NodelqdcselectNode2(la1Bz)))), concat(ite(isLeaf(ra1BA), cons(LeaflqdcselectLeaf1(ra1BA), nil), concat(flatten(NodelqdcselectNode1(ra1BA)), flatten(NodelqdcselectNode2(ra1BA)))), nsa1By))" +flattenRight2 :: RuntimeTerm flattenRight2 = "concat(concat(ite(isLeaf(la1Bz), cons(LeaflqdcselectLeaf1(la1Bz), nil), concat(flatten(NodelqdcselectNode1(la1Bz)), flatten(NodelqdcselectNode2(la1Bz)))), ite(isLeaf(ra1BA), cons(LeaflqdcselectLeaf1(ra1BA), nil), concat(flatten(NodelqdcselectNode1(ra1BA)), flatten(NodelqdcselectNode2(ra1BA))))), nsa1By)" +flattenSeq :: [RuntimeTerm] flattenSeq = [ "concat(flatten(la1Bz), concat(flatten(ra1BA), nsa1By))", "concat(ite(isLeaf(la1Bz), cons(LeaflqdcselectLeaf1(la1Bz), nil), concat(flatten(NodelqdcselectNode1(la1Bz)), flatten(NodelqdcselectNode2(la1Bz)))), concat(ite(isLeaf(ra1BA), cons(LeaflqdcselectLeaf1(ra1BA), nil), concat(flatten(NodelqdcselectNode1(ra1BA)), flatten(NodelqdcselectNode2(ra1BA)))), nsa1By))", "concat(concat(ite(isLeaf(la1Bz), cons(LeaflqdcselectLeaf1(la1Bz), nil), concat(flatten(NodelqdcselectNode1(la1Bz)), flatten(NodelqdcselectNode2(la1Bz)))), ite(isLeaf(ra1BA), cons(LeaflqdcselectLeaf1(ra1BA), nil), concat(flatten(NodelqdcselectNode1(ra1BA)), flatten(NodelqdcselectNode2(ra1BA))))), nsa1By)" ] +rpoSeq + :: (?impl::WQOConstraints impl m, Show (impl Op), Eq (impl Op), Hashable (impl Op)) + => [RuntimeTerm] + -> impl Op rpoSeq xs = go (OC.noConstraints ?impl) xs where - go c (t:u:xs) = OC.intersect ?impl c (rpoGTE t u) + go c (t:u:_xss) = OC.intersect ?impl c (rpoGTE t u) go c _ = c -tests :: (Hashable (oc Op), Eq (oc Op), Show (oc Op)) => (?impl :: OrderingConstraints oc IO) => [(String, IO Bool)] +tests :: (Hashable (oc Op), Eq (oc Op), Show (oc Op)) => (?impl :: WQOConstraints oc IO) => [(String, IO Bool)] tests = let f = Op "f" diff --git a/test/SMT.hs b/test/SMT.hs new file mode 100644 --- /dev/null +++ b/test/SMT.hs @@ -0,0 +1,30 @@ +module SMT where + +import Language.REST.SMT +import qualified Data.Map as M + +model :: String +model = "(\n\ + \ (define-fun op_j () Int \n\ + \ 1) \n\ + \(define-fun op_+ () Int \n\ + \ 2) \n\ + \(define-fun op_i () Int \n\ + \ 3) \n\ + \(define-fun op_s () Int \n\ + \ 4) \n\ + \(define-fun op_< () Int \n\ + \ 5) \n\ + \ )" + +expected :: M.Map String String +expected = M.fromList + [ ("op_j", "1") + , ("op_+", "2") + , ("op_i", "3") + , ("op_s", "4") + , ("op_<", "5") + ] + +tests :: [(String, Bool)] +tests = [("Parse SMT Model", parseModel model == expected)] diff --git a/test/StrictOC.hs b/test/StrictOC.hs --- a/test/StrictOC.hs +++ b/test/StrictOC.hs @@ -3,12 +3,11 @@ import Data.Maybe -import Language.REST.OrderingConstraints.Strict -import Language.REST.WQO -import Language.REST.Op -import DSL -import Language.REST.OpOrdering +import Language.REST.WQOConstraints.Strict +import Language.REST.Internal.WQO +import Language.REST.Internal.OpOrdering +tests :: [(String, Bool)] tests = [ ("permits", permits noConstraints wqo) diff --git a/test/Test.hs b/test/Test.hs --- a/test/Test.hs +++ b/test/Test.hs @@ -2,12 +2,15 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} module Main where +import qualified Data.List as L import Data.Hashable import Control.Monad.Identity import qualified Arith as A + import qualified Data.HashMap.Strict as M import OpOrdering import DSL @@ -15,38 +18,40 @@ import MultisetOrder as MultisetOrder import Nat import RPO as RPO +import KBO as KBO import StrictOC as StrictOC import LazyOC as LazyOC +import SMT as SMT import qualified QuickCheckTests as QuickCheckTests import System.IO -import Language.REST.AbstractOC + +import Language.REST.ExploredTerms +import Language.REST.OCAlgebra import Language.REST.OCToAbstract import Language.REST.Core -import Language.REST.OrderingConstraints as OC +import Language.REST.LPO (lpo) +import Language.REST.KBO (kbo) +import Language.REST.WQOConstraints as OC import Language.REST.Op import Language.REST.RPO -import Language.REST.OpOrdering +import Language.REST.Internal.OpOrdering import Language.REST.RuntimeTerm import Language.REST.MetaTerm as MT -import Language.REST.Rewrite +import Language.REST.Internal.Rewrite import Language.REST.Rest -import Language.REST.Path import Language.REST.SMT -import qualified Language.REST.OrderingConstraints.Lazy as LC -import qualified Language.REST.OrderingConstraints.Strict as SC -import qualified Language.REST.OrderingConstraints.ADT as AC -import Language.REST.WorkStrategy +import qualified Language.REST.WQOConstraints.ADT as AC +import Language.REST.Internal.WorkStrategy import qualified Data.Maybe as Mb import qualified Data.HashSet as S -diverges :: (Show oc) - => (?impl :: AbstractOC oc RuntimeTerm IO) => [RuntimeTerm] -> IO Bool -diverges ts = not <$> (isSat ?impl $ orient ts) +diverges :: (Show oc) => OCAlgebra oc RuntimeTerm IO -> [RuntimeTerm] -> IO Bool +diverges impl ts = not <$> (isSat impl $ orient impl ts) rewrites :: (Show oc, Hashable oc, Eq oc) - => (?impl :: AbstractOC oc RuntimeTerm IO) - => S.HashSet Rewrite -> S.HashSet Rewrite -> RuntimeTerm -> IO (S.HashSet RuntimeTerm) -rewrites evalRWs userRWs t0 = + => OCAlgebra oc RuntimeTerm IO + -> S.HashSet Rewrite -> S.HashSet Rewrite -> RuntimeTerm -> IO (S.HashSet RuntimeTerm) +rewrites impl evalRWs userRWs t0 = terms <$> fst <$> rest RESTParams { re = evalRWs @@ -56,7 +61,10 @@ , workStrategy = notVisitedFirst , ocImpl = ?impl , initRes = termsResult + , etStrategy = ExploreWhenNeeded } t0 + where + ?impl = impl runTest :: (String, IO Bool) -> IO () runTest (name, test) = do @@ -77,14 +85,14 @@ toTest = id runTestSuite :: Testable a => String -> [(String, a)] -> IO () -runTestSuite name tests = do +runTestSuite name tests1 = do putStrLn $ "Running test suite: " ++ name - mapM_ (runTest . go) tests + mapM_ (runTest . go) tests1 where - go (name, test) = (name, toTest test) + go (name1, test) = (name1, toTest test) -orderingTests :: (Hashable (oc Op), Show (oc Op), Ord (oc Op)) => (?impl :: OrderingConstraints oc IO) => [(String, IO Bool)] +orderingTests :: (Hashable (oc Op), Show (oc Op), Ord (oc Op)) => (?impl :: WQOConstraints oc IO) => [(String, IO Bool)] orderingTests = [ ("simple1", return $ not $ (rpoGTE "f(t1)" "g(t2)") `permits'` (t1Op =. t2Op)) @@ -96,26 +104,27 @@ where permits' = permits ?impl -proveEQ :: (Show oc, Hashable oc, Eq oc) => (?impl :: AbstractOC oc RuntimeTerm IO) - => S.HashSet Rewrite -> S.HashSet Rewrite -> RuntimeTerm -> RuntimeTerm -> IO Bool -proveEQ evalRWs userRWs have want = +proveEQ :: (Show oc, Hashable oc, Eq oc) => + OCAlgebra oc RuntimeTerm IO + -> S.HashSet Rewrite -> S.HashSet Rewrite + -> RuntimeTerm -> RuntimeTerm -> IO Bool +proveEQ impl evalRWs userRWs have want = do - rw1 <- (rewrites evalRWs userRWs have) - rw2 <- (rewrites evalRWs userRWs want) + rw1 <- (rewrites impl evalRWs userRWs have) + rw2 <- (rewrites impl evalRWs userRWs want) return $ not $ disjoint rw1 rw2 where disjoint s1 s2 = S.null $ s1 `S.intersection` s2 -arithTests :: (Show oc, Hashable oc, Eq oc) - => (?impl :: AbstractOC oc RuntimeTerm IO) => [(String, IO Bool)] -arithTests = +arithTests :: (Show oc, Hashable oc, Eq oc) => OCAlgebra oc RuntimeTerm IO -> [(String, IO Bool)] +arithTests impl = [ ("Contains", return $ contains (intToTerm 2) (intToTerm 1)) - , ("Diverge", not <$> (diverges [ (intToTerm 2) .+ t1 + , ("Diverge", not <$> (diverges impl [ (intToTerm 2) .+ t1 , (intToTerm 1) .+ t1 ] )) - , ("Diverge3", not <$> (diverges [ (t1 .+ t2) .+ t3 + , ("Diverge3", not <$> (diverges impl [ (t1 .+ t2) .+ t3 , t1 .+ (t2 .+ t3) , (t2 .+ t3) .+ t1 ] @@ -144,36 +153,36 @@ return $ termToInt t' == Just n - termTest = proveEQ evalRWs userRWs (App f [t1]) zero + termTest = proveEQ impl evalRWs userRWs (App f1 [t1]) zero where evalRWs = S.union termEvalRWs A.evalRWs - userRWs = S.insert (MT.RWApp g [x] ~> MT.RWApp f [x]) A.userRWs + userRWs = S.insert (MT.RWApp g1 [x] ~> MT.RWApp f1 [x]) A.userRWs termEvalRWs = S.fromList - [ MT.RWApp f [x] ~> MT.RWApp g [suc' x] - , MT.RWApp g [x] ~> zero' + [ MT.RWApp f1 [x] ~> MT.RWApp g1 [suc' x] + , MT.RWApp g1 [x] ~> zero' ] - f = Op "f" - g = Op "g" + f1 = Op "f" + g1 = Op "g" - termTest2 = proveEQ evalRWs userRWs (App f [zero]) (App g [zero]) + termTest2 = proveEQ impl evalRWs userRWs (App f1 [zero]) (App g1 [zero]) where - evalRWs = S.union termEvalRWs A.evalRWs - userRWs = S.insert (MT.RWApp f [x] ~> MT.RWApp g [(suc' (suc' x))]) A.userRWs + evalRWs = S.union termEvalRWs A.evalRWs + userRWs = S.insert (MT.RWApp f1 [x] ~> MT.RWApp g1 [(suc' (suc' x))]) A.userRWs termEvalRWs = S.fromList - [ MT.RWApp f [suc' x] ~> MT.RWApp g [suc' x] - , MT.RWApp f [zero'] ~> zero' - , MT.RWApp g [suc' x] ~> MT.RWApp f [x] - , MT.RWApp g [zero'] ~> zero' + [ MT.RWApp f1 [suc' x] ~> MT.RWApp g1 [suc' x] + , MT.RWApp f1 [zero'] ~> zero' + , MT.RWApp g1 [suc' x] ~> MT.RWApp f1 [x] + , MT.RWApp g1 [zero'] ~> zero' ] - f = Op "f" - g = Op "g" + f1 = Op "f" + g1 = Op "g" - eq = proveEQ A.evalRWs A.userRWs + eq = proveEQ impl A.evalRWs A.userRWs -completeTests :: (Show oc, Hashable oc, Eq oc) => (?impl :: AbstractOC oc RuntimeTerm IO) => [(String, IO Bool)] -completeTests = - [ ("CompleteDiverges", not <$> diverges [App start [], App mid [], App finish []]) +completeTests :: (Show oc, Hashable oc, Eq oc) => OCAlgebra oc RuntimeTerm IO -> [(String, IO Bool)] +completeTests impl = + [ ("CompleteDiverges", not <$> diverges impl [App start [], App mid [], App finish []]) , ("Complete1" , eq (App start []) (App finish [])) , ("EvalComplete2" , (== (App finish [])) <$> eval completeUserRWs (App start' [App s1 []]) ) , ("Complete2" , eq (App start' [App s1 []]) (App finish [])) @@ -190,7 +199,7 @@ ] eq :: RuntimeTerm -> RuntimeTerm -> IO Bool - eq = proveEQ S.empty completeUserRWs + eq = proveEQ impl S.empty completeUserRWs start = Op "start" mid = Op "mid" @@ -202,6 +211,7 @@ s1 = Op "s1" s2 = Op "s2" +ocTests :: (Handle, Handle) -> IO () ocTests z3 = do runTestSuite "LazyOC" LazyOC.tests runTestSuite "StrictOC" StrictOC.tests @@ -212,16 +222,29 @@ main :: IO () main = spawnZ3 >>= go where + + implTests implName impl toSkip = do + runTestSuite ("Arith" ++ implName) (withSkips $ arithTests impl) + runTestSuite ("Complete" ++ implName) (withSkips $ completeTests impl) + where + withSkips tests1 = do + (name, test) <- tests1 + guard $ L.notElem name toSkip + return (name, test) + + + go :: SolverHandle -> IO () go z3 = do putStrLn "Running REST Test Suite" - QuickCheckTests.tests + runTestSuite "SMT" SMT.tests + runTestSuite "KBO" (KBO.tests z3) + _ <- QuickCheckTests.tests runTestSuite "OpOrdering" OpOrdering.tests ocTests z3 runTestSuite "MultisetOrder" MultisetOrder.tests runTestSuite "WQO" WQO.tests - runTestSuite "Arith" arithTests - runTestSuite "Complete" completeTests + implTests "KBO" (kbo z3) [] + implTests "RPO" (lift (AC.adtOC z3) rpo) [] + implTests "LPO" (lift (AC.adtOC z3) lpo) ["Diverge3", "Arith4", "Arith4.1", "Arith6"] killZ3 z3 - where - ?impl = lift (AC.adtOC z3) rpo diff --git a/test/WQO.hs b/test/WQO.hs --- a/test/WQO.hs +++ b/test/WQO.hs @@ -1,6 +1,6 @@ module WQO where -import Language.REST.WQO as WQO +import Language.REST.Internal.WQO as WQO basicInvalid :: Maybe (WQO Char) basicInvalid = do diff --git a/test/WQODot.hs b/test/WQODot.hs new file mode 100644 --- /dev/null +++ b/test/WQODot.hs @@ -0,0 +1,21 @@ +module WQODot where + +import Data.Hashable +import qualified Data.Set as S + +import Language.REST.Dot +import Language.REST.Internal.PartialOrder +import Language.REST.Internal.WQO + +toDigraph :: (Ord a, Hashable a, Show a) => WQO a -> DiGraph +toDigraph wqo = digraph where + + digraph = DiGraph "wqo" nodes edges + + labelFor ec = 'n' : show (abs $ hash ec) + + nodes = S.map toNode (getECs wqo) + edges = S.fromList $ map toEdge (toList $ getPO wqo) + + toNode ec = Node (labelFor ec) (show ec) "solid" "black" + toEdge (ec1, ec2) = Edge (labelFor ec1) (labelFor ec2) "" "black" "" "solid" diff --git a/testlib/Arith.hs b/testlib/Arith.hs new file mode 100644 --- /dev/null +++ b/testlib/Arith.hs @@ -0,0 +1,53 @@ +{-# LANGUAGE OverloadedStrings #-} +module Arith where + +import DSL +import Language.REST.Internal.Rewrite (Rewrite) +import Language.REST.MetaTerm +import Language.REST.Op + +import qualified Data.HashSet as S + +neg :: MetaTerm -> MetaTerm +neg x1 = RWApp (Op "neg") [x1] + +double :: MetaTerm -> MetaTerm +double x1 = RWApp (Op "double") [x1] + +twicePlus :: MetaTerm -> MetaTerm -> MetaTerm +twicePlus x1 y1 = RWApp (Op "twicePlus") [x1, y1] + +(<#) :: MetaTerm -> MetaTerm -> MetaTerm +x1 <# y1 = RWApp (Op "<") [x1, y1] + +evalRWs :: S.HashSet Rewrite +evalRWs = + S.fromList + [ + (suc' x) <# (suc' y) ~> x <# y + , (suc' x) #+ y ~> suc' (x #+ y) + , zero' #+ x ~> x + + , (suc' x) #* y ~> y #+ (x #* y) + , zero' #* y ~> zero' + + , ack' zero' x ~> suc' x + , ack' (suc' x) zero' ~> ack' x one' + , ack' (suc' x) (suc' y) ~> ack' x (ack' (suc' x) y) + , double x ~> x #+ x + , twicePlus x y ~> (x #+ x) #+ y + ] + +userRWs :: S.HashSet Rewrite +userRWs = + S.fromList $ + [ x #+ y ~> y #+ x + + , x #* y ~> y #* x + + , (x #+ y) #* v ~> (x #* v) #+ (y #* v) + , (neg x) #+ x ~> zero' + -- , (x #* v) #+ (y #* v) ~> (x #+ y) #* v + + -- , x ~> x #+ zero' + ] ++ [ x #+ (y #+ v) ~> (x #+ y) #+ v] diff --git a/testlib/DSL.hs b/testlib/DSL.hs new file mode 100644 --- /dev/null +++ b/testlib/DSL.hs @@ -0,0 +1,100 @@ +{-# LANGUAGE OverloadedStrings #-} + +module DSL where + +import Language.REST.Op +import qualified Language.REST.MetaTerm as MT +import Language.REST.RuntimeTerm as RT +import Language.REST.Internal.Rewrite +import Nat + +commutes, assocL, assocR :: (MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm) -> Rewrite +commutes op = x `op` y ~> y `op` x +assocL op = (x `op` y) `op` z' ~> x `op` (y `op` z') +assocR op = x `op` (y `op` z') ~> (x `op` y) `op` z' + +distribL, distribR + :: (MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm) + -> (MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm) + -> Rewrite +distribL op1 op2 = (x `op1` y) `op2` z' ~> (x `op2` z') `op1` (y `op2` z') +distribR op1 op2 = z' `op2` (x `op1` y) ~> (z' `op2` x) `op1` (z' `op2` y) + +ackOp, plus, minus, times :: Op +ackOp = Op "ack" +plus = Op "+" +minus = Op "-" +times = Op "*" + +a, b, c, d :: RuntimeTerm +a = App (Op "a") [] +b = App (Op "b") [] +c = App (Op "c") [] +d = App (Op "d") [] + +x, y, v, w, z' :: MT.MetaTerm +x = MT.Var "x" +y = MT.Var "y" +v = MT.Var "v" +w = MT.Var "w" +z' = MT.Var "z" + +f, g, h :: Op +f = Op "f" +g = Op "g" +h = Op "h" + +t1Op, t2Op :: Op +t1Op = Op "t1" +t2Op = Op "t2" + +t1, t2, t3, t4, t5 :: RuntimeTerm +t1 = App (Op "t1") [] +t2 = App (Op "t2") [] +t3 = App (Op "t3") [] +t4 = App (Op "t4") [] +t5 = App (Op "t5") [] + +zero, one, two :: RuntimeTerm +zero = App z [] +one = suc zero +two = suc one + +suc :: RuntimeTerm -> RuntimeTerm +suc x1 = App s [x1] + +ack :: RuntimeTerm -> RuntimeTerm -> RuntimeTerm +ack x1 y1 = App ackOp [x1, y1] + +zero' :: MT.MetaTerm +zero' = MT.toMetaTerm zero + +one' :: MT.MetaTerm +one' = suc' zero' + +suc' :: MT.MetaTerm -> MT.MetaTerm +suc' x1 = MT.RWApp s [x1] + +ack' :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm +ack' x1 y1 = MT.RWApp ackOp [x1, y1] + +infixl 1 .+ +(.+) :: RuntimeTerm -> RuntimeTerm -> RuntimeTerm +(.+) x1 y1 = App plus [x1, y1] + +(#+) :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm +(#+) x1 y1 = MT.RWApp plus [x1, y1] + +(#-) :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm +(#-) x1 y1 = MT.RWApp minus [x1, y1] + +(#*) :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm +(#*) x1 y1 = MT.RWApp times [x1, y1] + +infix 0 ~> +(~>) :: MT.MetaTerm -> MT.MetaTerm -> Rewrite +t ~> u = Rewrite t u Nothing + +infix 0 <~> +(<~>) :: MT.MetaTerm -> MT.MetaTerm -> [Rewrite] +t <~> u = [ t ~> u, u ~> t ] diff --git a/testlib/Language/REST/ConcreteOC.hs b/testlib/Language/REST/ConcreteOC.hs new file mode 100644 --- /dev/null +++ b/testlib/Language/REST/ConcreteOC.hs @@ -0,0 +1,59 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} + +module Language.REST.ConcreteOC where + +import qualified Language.REST.OCAlgebra as AOC +import qualified Language.REST.Internal.WQO as WQO +import Language.REST.RuntimeTerm +import Language.REST.RPO +import Language.REST.Internal.OpOrdering +import Language.REST.MetaTerm + +import Data.List as L +import Data.Hashable +import GHC.Generics (Generic) +import qualified Data.Set as S + +data ConcreteOC = ConcreteOC [RuntimeTerm] (Maybe OpOrdering) + deriving (Eq, Ord, Generic, Hashable) + +instance Show ConcreteOC where + show (ConcreteOC _ (Just oo)) = show oo + show _ = "impossible" + +isSat :: ConcreteOC -> Bool +isSat (ConcreteOC _ (Just _)) = True +isSat _ = False + +getOrdering :: [RuntimeTerm] -> Maybe OpOrdering +getOrdering ts = + let + ops = S.unions $ map termOps ts + orderings = S.toList $ WQO.orderings ops + in + L.find (`orients` ts) orderings + + +orients :: OpOrdering -> [RuntimeTerm] -> Bool +orients ordering terms = + let + pairs = zip terms (tail terms) + in + all (uncurry $ synGTE ordering) pairs + +concreteOC :: Monad m => AOC.OCAlgebra ConcreteOC RuntimeTerm m +concreteOC = AOC.OCAlgebra (return . isSat) refine (ConcreteOC [] (Just (WQO.empty))) constUnion notStrongerThan + where + constUnion t1 _ = t1 + notStrongerThan _ _ = return False + refine :: ConcreteOC -> RuntimeTerm -> RuntimeTerm -> ConcreteOC + refine (ConcreteOC ts (Just o)) _ u = + let + ts' = ts ++ [u] + in + ConcreteOC ts' $ + if o `orients` ts' + then Just o + else getOrdering ts' + refine (ConcreteOC ts Nothing) _ u = ConcreteOC (ts ++ [u]) Nothing diff --git a/testlib/Language/REST/ProofGen.hs b/testlib/Language/REST/ProofGen.hs new file mode 100644 --- /dev/null +++ b/testlib/Language/REST/ProofGen.hs @@ -0,0 +1,57 @@ +{-# LANGUAGE OverloadedStrings #-} +module Language.REST.ProofGen where + +import qualified Data.HashMap.Strict as M +import qualified Data.List as L +import qualified Data.Text as T +import Text.Printf + +import Language.REST.Path +import Language.REST.Internal.Rewrite +import Language.REST.RuntimeTerm +import Language.REST.Op + +-- Hardcoded +opToLH :: Op -> String +opToLH (Op "union") = "mp" +opToLH (Op "toMS") = "multiset_of" +opToLH (Op op) = T.unpack op + +withParens :: Bool -> String -> String +withParens True t = "(" ++ t ++ ")" +withParens False t = t + +toLH :: Bool -> RuntimeTerm -> String +-- Hardcoded rules +toLH parens (App "m" [arg]) = withParens parens $ printf "Multiset [%s]" (toLH False arg) +toLH parens (App "cons" [x, xs]) = withParens parens $ printf "%s:%s" (toLH True x) (toLH True xs) + +toLH _ (App op []) = opToLH op +toLH parens (App op args) = + withParens parens $ printf "%s %s" (opToLH op) (L.intercalate " " $ map (toLH True) args) + +toProof :: Path Rewrite RuntimeTerm a -> String +toProof (steps, PathTerm result _) = " " ++ (L.intercalate "\n=== " $ proofSteps ++ [toLH False result]) ++ "\n*** QED" + where + proofSteps :: [String] + proofSteps = map proofStep $ zip steps [0..] + + proofStep ((Step (PathTerm t _) _ _ True), _) = toLH False t + proofStep ((Step (PathTerm t _) (Rewrite lhs rhs name) _ False), i) = toLH False t ++ " ? " ++ toLemma lemma + where + lemma = go (subTerms t) + + lemmaName = + case name of + Just n -> T.pack n + Nothing -> "lemma" + + toLemma s = toLH False (App (Op lemmaName) (map snd $ L.sort $ M.toList s)) + + go [] = undefined + go ((st, f): _) | Just su <- unify lhs st M.empty + , f (subst su rhs) == nextTerm + = su + go (_:xs) = go xs + + nextTerm = if i < (length steps - 1) then (pathTerm . term) (steps !! (i + 1)) else result diff --git a/testlib/MultisetOrdering.hs b/testlib/MultisetOrdering.hs new file mode 100644 --- /dev/null +++ b/testlib/MultisetOrdering.hs @@ -0,0 +1,145 @@ +{-# LANGUAGE ScopedTypeVariables#-} +module MultisetOrdering where + +import Data.Hashable +import Language.REST.Dot +import qualified Data.Maybe as Mb +import qualified Data.List as L +import qualified Language.REST.Internal.MultiSet as M +import qualified Data.HashMap.Strict as Mp +import qualified Data.HashSet as S +import Language.REST.Types + +data Replace a = + ReplaceOne a a + | Replace a [a] + deriving (Show) + +data MultisetGE a = MultisetGE [Replace a] deriving (Show) + +type GTE a = a -> a -> Bool + +type Indexed a = (a, Int) + +type IndexedMultisetPair a = (Indexed (M.MultiSet (Indexed a)) , Indexed (M.MultiSet (Indexed a))) + +multisetGE :: forall a . Eq a => GTE a -> M.MultiSet a -> M.MultiSet a -> Maybe (MultisetGE a) +multisetGE gte ts0 us0 = go [] (M.toList ts0) (M.toList us0) + where + equiv t u = t `gte` u && u `gte` t + gt t u = t `gte` u && not (u `gte` t) + + go :: [Replace a] -> [a] -> [a] -> Maybe (MultisetGE a) + go rs (t : ts) us | Just u <- L.find (equiv t) us + = go ((ReplaceOne t u):rs) ts (L.delete u us) + + go rs (t : ts) us | otherwise = + let + (lts, us') = L.partition (t `gt`) us + in + go ((Replace t lts) : rs) ts us' + go rs ts [] = Just $ MultisetGE $ (map ((flip Replace) []) ts) ++ rs + go _ [] _ = Nothing + + +multisetOrd :: (Eq a, Hashable a, Ord a) => [a] -> [a] -> Maybe (MultisetGE a) +multisetOrd ts us = multisetGE (>=) (M.fromList ts) (M.fromList us) + +zindex :: [a] -> [(a, Int)] +zindex xs = zip xs [0 ..] + +indexMS :: (Eq a, Hashable a) => M.MultiSet a -> M.MultiSet (a, Int) +indexMS ms = M.fromList $ zindex (M.toList ms) + +mkEdge :: NodeID -> NodeID -> Edge +mkEdge t u = Edge t u " " "black" " " "solid" + +botNodeName :: Int -> Int -> String +botNodeName tIndex mIndex = "bot_" ++ show tIndex ++ "_" ++ show mIndex + +botNode :: Int -> Int -> Node +botNode tIndex mIndex = + Node (botNodeName tIndex mIndex) "⊥" "solid" "black" + +toGraph' :: forall a. (Eq a, Hashable a, Show a) => GTE a -> [M.MultiSet a] -> DiGraph +toGraph' gte mss0 = DiGraph "msograph" (toOrderedSet (S.union elemNodes botNodes)) (toOrderedSet edges) + where + indexed :: [(M.MultiSet (a, Int), Int)] + indexed = zindex (map indexMS mss0) + + pairs :: [((M.MultiSet (a, Int), Int), (M.MultiSet (a, Int), Int))] + pairs = zip indexed (tail indexed) + + elemNodes = S.fromList $ filter hasEdge $ concatMap toNodes indexed + + hasEdge node = any (`pointsTo` node) $ S.toList edges + + pointsTo edge node = + from edge == nodeID node || to edge == nodeID node + + edges :: S.HashSet Edge + edges = S.fromList $ topEdges ++ (map snd $ replEdges pairs) + + topEdges = map go (M.toList (fst $ head indexed)) where + go (_, index) = + mkEdge "⊤" (nodeName (index, 0)) + + botNodes = S.fromList $ concatMap Mb.maybeToList $ map fst $ replEdges pairs + + nodeName :: (Int, Int) -> String + nodeName (elemIndex, msIndex) = + "n" ++ show elemIndex ++ "_" ++ show msIndex + + replEdges = toEdges Mp.empty + + toEdges :: Mp.HashMap (Int, Int) (Int, Int) -> [IndexedMultisetPair a] -> ([(Maybe Node, Edge)]) + toEdges _ [] = [] + toEdges mp (((ts, tsIndex), (us, usIndex)) : mss) = + concatMap redges repls ++ toEdges mp' mss + where + Just (MultisetGE repls) = multisetGE (\t u -> gte (fst t) (fst u)) ts us + + lookupTIndex :: Int -> (Int, Int) + lookupTIndex tindex = case Mp.lookup (tindex, tsIndex) mp of + Just t -> t + Nothing -> (tindex, tsIndex) + + mp' = go mp repls where + go mpi [] = mpi + go mpi ((ReplaceOne (_, i) (_, j)):repls') + = go (Mp.insert (j, usIndex) (lookupTIndex i) mpi) repls' + go mpi (_:repls') = go mpi repls' + + + redges (Replace (_, index) []) + = [ ( Just (botNode index tsIndex) + , mkEdge + (nodeName (lookupTIndex index)) + (botNodeName index tsIndex) + ) ] + redges (ReplaceOne _ _) = [] + redges (Replace (_, tindex) us') = map go us' where + go (_, uindex) = + (Nothing, mkEdge (nodeName (lookupTIndex tindex)) (nodeName (uindex, usIndex))) + + toNodes (ms, index) = map go (M.toList ms) where + + go (e, elemIndex) = + Node + (nodeName (elemIndex, index)) + (show e) + "solid" + "black" + +toGraph :: (Ord a, Eq a, Hashable a, Show a) => [[a]] -> DiGraph +toGraph mss = toGraph' (>=) $ map M.fromList mss + +mkMSOGraph :: (Ord a, Eq a, Hashable a, Show a) => String -> [[a]] -> IO () +mkMSOGraph name mss = mkGraph name (toGraph mss) + +mkMSOGraphs :: (Ord a, Eq a, Hashable a, Show a) => String -> [[a]] -> IO () +mkMSOGraphs name mss0 = mapM_ go (drop 1 $ L.inits mss0) where + go mss = mkGraph (name ++ show (length mss)) (toGraph mss) + +multisetGE' :: (Ord a, Hashable a) => [a] -> [a] -> Maybe (MultisetGE a) +multisetGE' ts us = multisetGE (>=) (M.fromList ts) (M.fromList us) diff --git a/testlib/Nat.hs b/testlib/Nat.hs new file mode 100644 --- /dev/null +++ b/testlib/Nat.hs @@ -0,0 +1,103 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Nat (termToInt, intToTerm, parseTerm, pp, s, z) where + + +import Data.Text +import Text.Parsec (Parsec, ParsecT, Stream) +import Text.ParserCombinators.Parsec.Char +import Text.ParserCombinators.Parsec +import Data.String + +import qualified Language.REST.MetaTerm as MT +import Language.REST.Op +import Language.REST.Types +import Language.REST.RuntimeTerm as RT + +z, s :: Op +s = Op "s" +z = Op "z" + +intToTerm :: Int -> RuntimeTerm +intToTerm 0 = App z [] +intToTerm n = App s [intToTerm (n - 1)] + +termToInt :: (MT.ToMetaTerm a) => a -> Maybe Int +termToInt t = go (MT.toMetaTerm t) where + go (MT.RWApp mop []) | mop == z = Just 0 + go (MT.RWApp mop [t1]) | mop == s = (1 +) <$> go t1 + go _ = Nothing + +instance ToRuntimeTerm Int where + toRuntimeTerm = intToTerm + +pp :: MT.ToMetaTerm a => a -> String +pp = prettyPrint (PPArgs [] + [ ("<", "<") + , ("+", "+") + , ("*", "*") + , ("∪", "∪") + , ("union", "∪") + , ("intersect", "∩") + ] showInt) + where + showInt :: MT.MetaTerm -> Maybe Text + showInt t = fmap (pack . show) $ termToInt t + +op :: GenParser Char st Op +op = fmap (Op . pack) (many (alphaNum <|> char '\'')) + +parens :: Stream s m Char => ParsecT s u m b -> ParsecT s u m b +parens p = do + _ <- char '(' + r <- p + _ <- char ')' + return r + +term :: Parsec String u RuntimeTerm +term = try infixTerm <|> nonInfixTerm + where + + nonInfixTerm = try (parens term) <|> try appTerm <|> try numberTerm <|> nullTerm + + numberTerm = do + d1 <- digit + n <- many digit + return $ intToTerm (read (d1 : n)) + + infixOp = + try (string "+") + <|> try (string "<") + <|> (try (string "\\/") >> return "∪") + <|> string "*" + + infixTerm = do + t1 <- nonInfixTerm + _ <- spaces + top <- infixOp + _ <- spaces + t2 <- nonInfixTerm + return $ App (Op (pack top)) [t1, t2] + + nullTerm = do + o <- op + return $ App o [] + + appTerm = do + o <- op + trms <- parens $ sepBy1 term (char ',' >> spaces) + return $ App o trms + + +parseTerm :: String -> RuntimeTerm +parseTerm str = + case parse term "" str of + Left err -> error (show err) + Right t -> t + +instance IsString RuntimeTerm where + fromString = parseTerm diff --git a/testlib/Set.hs b/testlib/Set.hs new file mode 100644 --- /dev/null +++ b/testlib/Set.hs @@ -0,0 +1,60 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Set where + +import Arith as A +import DSL +import Language.REST.Internal.Rewrite (Rewrite) +import Language.REST.MetaTerm + +import qualified Data.HashSet as S + +emptyset :: MetaTerm +emptyset = RWApp "∅" [] + +(/\), (\/) :: MetaTerm -> MetaTerm -> MetaTerm +x1 /\ y1 = RWApp "intersect" [x1, y1] +x1 \/ y1 = RWApp "union" [x1, y1] + +s0, s1 :: MetaTerm +s0 = RWApp "s₀" [] +s1 = RWApp "s₁" [] + +isSubset :: MetaTerm -> MetaTerm -> Rewrite +isSubset mt1 mt2 = mt1 \/ mt2 ~> mt2 + +userRWs :: S.HashSet Rewrite +userRWs = S.union A.evalRWs $ S.fromList $ + [ + distribL (/\) (\/) + , distribR (/\) (\/) + , distribL (\/) (/\) + , distribR (\/) (/\) + , assocL (\/) + , assocL (/\) + , x /\ x ~> x + , x \/ x ~> x + , x \/ emptyset ~> x + , commutes (\/) + , commutes (/\) + + -- Example 1 + -- , s1 /\ s0 ~> emptyset + + -- Example 2 + , s0 \/ s1 ~> s0 + ] + +evalRWs :: S.HashSet Rewrite +evalRWs = S.union A.userRWs $ S.fromList -- + [ RWApp "t2" [] ~> emptyset + , isSubset (RWApp "right1" []) (RWApp "right" []) + ] + +disjointExample, disjointExample2 :: String +disjointExample = "union(union(left, right1), union(left,right))" +disjointExample2 = "union(left, union(right1, union(left,right)))" + +example1, example2 :: String +example1 = "f(intersect(union(s₀,s₁), s₀))" +example2 = "f(union(intersect(s₀,s₁), s₀))"