rest-rewrite 0.1.1 → 0.4.5
raw patch · 89 files changed
Files
- graphs/.DONOTDELETE +0/−0
- rest-rewrite.cabal +71/−102
- src/Arith.hs +0/−41
- src/BagExample.hs +0/−114
- src/Compiler.hs +0/−29
- src/DSL.hs +0/−77
- src/Group.hs +0/−23
- src/Language/REST.hs +6/−38
- src/Language/REST/AbstractOC.hs +0/−32
- src/Language/REST/ConcreteOC.hs +0/−57
- src/Language/REST/Core.hs +10/−56
- src/Language/REST/Dot.hs +39/−17
- src/Language/REST/EquivalenceClass.hs +0/−73
- src/Language/REST/ExploredTerms.hs +66/−35
- src/Language/REST/Internal/EquivalenceClass.hs +81/−0
- src/Language/REST/Internal/ListT.hs +43/−0
- src/Language/REST/Internal/MultiSet.hs +87/−0
- src/Language/REST/Internal/MultisetOrder.hs +85/−0
- src/Language/REST/Internal/OpOrdering.hs +97/−0
- src/Language/REST/Internal/Orphans.hs +34/−0
- src/Language/REST/Internal/PartialOrder.hs +139/−0
- src/Language/REST/Internal/Rewrite.hs +75/−0
- src/Language/REST/Internal/Util.hs +15/−0
- src/Language/REST/Internal/WQO.hs +358/−0
- src/Language/REST/Internal/WorkStrategy.hs +39/−0
- src/Language/REST/KBO.hs +50/−0
- src/Language/REST/LPO.hs +92/−0
- src/Language/REST/MetaTerm.hs +2/−7
- src/Language/REST/MultiSet.hs +0/−80
- src/Language/REST/MultisetOrder.hs +0/−79
- src/Language/REST/OCAlgebra.hs +59/−0
- src/Language/REST/OCToAbstract.hs +12/−20
- src/Language/REST/Op.hs +3/−1
- src/Language/REST/OpOrdering.hs +0/−104
- src/Language/REST/OrderingConstraints.hs +0/−113
- src/Language/REST/OrderingConstraints/ADT.hs +0/−244
- src/Language/REST/OrderingConstraints/Lazy.hs +0/−118
- src/Language/REST/OrderingConstraints/Strict.hs +0/−152
- src/Language/REST/PartialOrder.hs +0/−98
- src/Language/REST/Path.hs +14/−7
- src/Language/REST/ProofGen.hs +0/−55
- src/Language/REST/RESTDot.hs +37/−17
- src/Language/REST/RPO.hs +51/−70
- src/Language/REST/Rest.hs +53/−42
- src/Language/REST/Rewrite.hs +0/−56
- src/Language/REST/RewriteRule.hs +5/−0
- src/Language/REST/RuntimeTerm.hs +25/−6
- src/Language/REST/SMT.hs +217/−32
- src/Language/REST/Types.hs +19/−14
- src/Language/REST/WQO.hs +0/−329
- src/Language/REST/WQOConstraints.hs +132/−0
- src/Language/REST/WQOConstraints/ADT.hs +227/−0
- src/Language/REST/WQOConstraints/Lazy.hs +120/−0
- src/Language/REST/WQOConstraints/Strict.hs +141/−0
- src/Language/REST/WorkStrategy.hs +0/−37
- src/Lists.hs +0/−34
- src/Main.hs +0/−151
- src/Multiset.hs +0/−44
- src/MultisetOrdering.hs +0/−141
- src/Nat.hs +0/−99
- src/NonTerm.hs +0/−29
- src/Set.hs +0/−53
- src/WQODot.hs +0/−21
- test/BagExample.hs +117/−0
- test/Compiler.hs +35/−0
- test/ExploredTerms.hs +45/−0
- test/Group.hs +26/−0
- test/KBO.hs +21/−0
- test/LazyOC.hs +16/−0
- test/Lists.hs +40/−0
- test/Main.hs +193/−0
- test/Multiset.hs +57/−0
- test/MultisetOrder.hs +9/−7
- test/NonTerm.hs +28/−0
- test/OpOrdering.hs +10/−10
- test/QuickCheckTests.hs +29/−18
- test/RPO.hs +23/−14
- test/SMT.hs +30/−0
- test/StrictOC.hs +11/−12
- test/Test.hs +115/−72
- test/WQO.hs +3/−2
- test/WQODot.hs +21/−0
- testlib/Arith.hs +53/−0
- testlib/DSL.hs +100/−0
- testlib/Language/REST/ConcreteOC.hs +32/−0
- testlib/Language/REST/ProofGen.hs +54/−0
- testlib/MultisetOrdering.hs +143/−0
- testlib/Nat.hs +103/−0
- testlib/Set.hs +60/−0
+ graphs/.DONOTDELETE view
rest-rewrite.cabal view
@@ -1,15 +1,18 @@ name: rest-rewrite build-type: Simple-version: 0.1.1-cabal-version: 1.22+version: 0.4.5+cabal-version: 2.0 category: Rewriting maintainer: Zack Grannan <zgrannan@cs.ubc.ca> author: Zack Grannan <zgrannan@cs.ubc.ca> license: BSD3-description: Rewriting library with online termination checking.+description: REST is a Rewriting library with online termination checking. For more details see the paper at https://arxiv.org/abs/2202.05872. synopsis: Rewriting library with online termination checking license-file: LICENSE +extra-source-files:+ graphs/.DONOTDELETE+ source-repository head type: git location: https://github.com/zgrannan/rest@@ -18,156 +21,122 @@ 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.ListT+ Language.REST.Internal.MultiSet+ Language.REST.Internal.MultisetOrder+ Language.REST.Internal.OpOrdering+ Language.REST.Internal.Orphans+ 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- , hashable >= 1.3.0 && < 1.4+ , containers >= 0.6.2 && < 0.8+ , hashable >= 1.3.0 && < 1.6 , process >= 1.6.9 && < 1.7 , parsec >= 3.1.14 && < 3.2- , mtl >= 2.2.2 && < 2.3+ , mtl >= 2.2.2 && < 2.4 , unordered-containers >= 0.2.13 && < 0.3- , text >= 1.2.4 && < 1.3+ , text >= 1.2.4 && < 2.2 +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+ , time >= 1.9.3 && < 1.15+ 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+ ExploredTerms+ 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- , text >= 1.2.2- , time >= 1.9.3 && < 1.10+ , testlib+ , text+ , time -- , 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
− src/Arith.hs
@@ -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]
− src/BagExample.hs
@@ -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)
− src/Compiler.hs
@@ -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 [ ]
− src/DSL.hs
@@ -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 ]
− src/Group.hs
@@ -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)- ]
src/Language/REST.hs view
@@ -2,48 +2,16 @@ module Language.REST where -import Control.Monad.Identity-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.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 System.IO (Handle) +-- | 'adtRPO' Is an ordering constraint algebra derived from the recursive+-- path ordering; it is a useful general-purpose OCA.+adtRPO :: (Handle, Handle) -> OCAlgebra (ConstraintsADT Op) RuntimeTerm IO adtRPO z3 = lift (adtOC z3) rpo--- lazyRPO = lift lazyOC rpo--- strictRPO = lift strictOC rpo---- 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)---varsEQ :: RuntimeTerm -> RuntimeTerm -> WQO.WQO Op-varsEQ t1 t2 =- let- vars = getVars t1 `S.union` getVars t2- in- fromJust $ WQO.mergeAll (map (uncurry (=.)) (pairs (S.toList vars)))- where- pairs xs | length xs < 2 = []- pairs xs | otherwise = zip xs (tail xs)--cgen :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RuntimeTerm Identity-cgen impl r oc t1 t2 =- let- Identity rpoc = rpo impl r oc t1 t2- in- return $ addConstraint impl (varsEQ t1 t2) rpoc
− src/Language/REST/AbstractOC.hs
@@ -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)
− src/Language/REST/ConcreteOC.hs
@@ -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
src/Language/REST/Core.hs view
@@ -1,63 +1,17 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE ImplicitParams #-} +-- | Core REST functions module Language.REST.Core where -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.Types-import qualified Language.REST.MetaTerm as MT-import Language.REST.WQO-import Language.REST.Rewrite-import Language.REST.RuntimeTerm as RT-import Language.REST.RewriteRule--type MetaTerm = MT.MetaTerm---contains :: RuntimeTerm -> RuntimeTerm -> Bool-contains t1 t2 | t1 == t2 = True-contains (App _ ts) t = any (contains t) ts-+import Language.REST.OCAlgebra+import Language.REST.RuntimeTerm -orient' :: Show oc => (?impl :: AbstractOC oc RuntimeTerm m) => oc -> [RuntimeTerm] -> oc-orient' oc0 ts0 = go oc0 (zip ts0 (tail ts0))- where+-- | @orient impl ts@ generates the constraints on an ordering defined by the+-- OCA `impl`, that ensures each term in the path `ts` is smaller than or+-- equal to the previous one.+orient :: OCAlgebra oc RuntimeTerm m -> [RuntimeTerm] -> oc+orient impl ts0 = go (top impl) (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)--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)--syms :: MetaTerm -> S.HashSet String-syms (MT.Var s) = S.singleton s-syms (MT.RWApp _ xs) = S.unions (map syms xs)--termPathStr :: [RuntimeTerm] -> String-termPathStr terms = L.intercalate " --> \n" (map pp terms)- where- pp = prettyPrint (PPArgs [] [] (const Nothing))--eval :: S.HashSet Rewrite -> RuntimeTerm -> IO RuntimeTerm-eval rws t =- do- result <- mapM (apply t) (S.toList rws)- case S.toList $ S.unions result of- [] -> return t- (t : _) -> eval rws t+ go oc ((t0, t1):ts) = go (refine impl oc t0 t1) ts
src/Language/REST/Dot.hs view
@@ -2,7 +2,15 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE ScopedTypeVariables #-} -module Language.REST.Dot where+-- | This module contains functionality for generating GraphViz graphs+module Language.REST.Dot+ ( mkGraph+ , DiGraph(..)+ , Edge(..)+ , GraphType(..)+ , Node(..)+ , NodeID+ ) where import GHC.Generics import Data.Hashable@@ -11,19 +19,32 @@ import Text.Printf import System.Process -data DiGraph = DiGraph String (S.Set Node) (S.Set Edge);+-- | A GraphViz directed graph+data DiGraph = DiGraph+ String -- ^ Filename+ (S.Set Node)+ (S.Set Edge); type NodeID = String -data GraphType = Tree | Dag | Min deriving (Read)+-- | The way the graph will be rendered+data GraphType =+ Tree -- ^ Standard representation+ | Dag -- ^ In 'Dag', If two equal terms `n` steps from the root are the same, they are+ -- represented by the same node, even if they were reached via different+ -- paths+ | Min -- ^ Each unique term is represented by the same node+ deriving (Read) -data Node = Node +-- | A GraphViz node+data Node = Node { nodeID :: NodeID , label :: String , nodeStyle :: String , labelColor :: String } deriving (Eq, Ord, Show, Generic, Hashable) +-- A GraphViz edge data Edge = Edge { from :: NodeID , to :: NodeID@@ -33,32 +54,31 @@ , edgeStyle :: String } deriving (Eq, Ord, Show, Generic, Hashable) -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) = - let - sub = escape subLabel- escape xs = concatMap go xs+edgeString (Edge efrom eto elabel color esubLabel style) =+ let+ sub = escape esubLabel+ escape = concatMap go where go '\\' = "\\" go '\n' = "<br />" go '>' = ">"+ go '<' = "<" go o = [o] labelPart =- if label /= ""- then printf "<font color =\"red\">%s</font>" label+ if elabel /= ""+ then printf "<font color =\"red\">%s</font>" (escape elabel) else "" in- printf "\t%s -> %s [label = <%s<br/>%s>\ncolor=\"%s\"\nstyle=\"%s\"];" from to labelPart sub color style+ printf "\t%s -> %s [label = <%s<br/>%s>\ncolor=\"%s\"\nstyle=\"%s\"];" efrom eto labelPart sub color style graphString :: DiGraph -> String-graphString (DiGraph name nodes edges) = - printf "digraph %s {\n%s\n\n%s\n}" name (nodesString) (edgesString)+graphString (DiGraph name nodes edges) =+ printf "digraph %s {\n%s\n\n%s\n}" name nodesString edgesString where nodesString :: String nodesString = intercalate "\n" (map nodeString (S.toList nodes))@@ -67,6 +87,8 @@ edgesString = intercalate "\n" (map edgeString (S.toList edges)) +-- | @mkGraph name graph@ generates the @.dot@ file for @graph@, and renders+-- the resulting graph to a @png@ file using the @dot@ utility mkGraph :: String -> DiGraph -> IO () mkGraph name graph = do let dotfile = printf "graphs/%s.dot" name
− src/Language/REST/EquivalenceClass.hs
@@ -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
src/Language/REST/ExploredTerms.hs view
@@ -1,5 +1,8 @@ {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE ScopedTypeVariables #-}+-- | This module implements the optimizations to prune the+-- exploration of rewrites of terms that have been already considered+-- (section 6.4 of the REST paper). module Language.REST.ExploredTerms ( ExploredTerms@@ -9,74 +12,104 @@ , size , visited , ExploreFuncs(..)+ , ExploreStrategy(..) ) where -import Debug.Trace import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S import Data.Hashable import Prelude hiding (lookup) +-- | 'ExploreStrategy' defines how 'shouldExplore' should decide whether or not+-- | to consider rewrites from a given term data ExploreStrategy =- ExploreAlways | ExploreLessConstrained | ExploreWhenNeeded | ExploreOnce+ ExploreAlways -- ^ Always explore, even when it's not necessary.+ | ExploreLessConstrained -- ^ Explore terms unless the constraints are stricter.+ -- This may stil explore unnecessary paths, the terms+ -- were already fully explored with the different constraints.+ | ExploreWhenNeeded -- ^ Explore terms unless the constraints are stricter OR if all+ -- terms reachable via transitive rewrites were already explored.+ | ExploreOnce -- ^ Explore each term only once. This may cause some terms not to be+ -- explored if the terms leading to them were initially visited at+ -- strict constraints. -data ExploreFuncs c m = EF- { union :: c -> c -> c++data ExploreFuncs term c m = EF+ { -- | When a term @t@ is visited at constraints @c0@, and then at constraints+ -- @c1@, the constraints for term @t@ is set to @c0 `union` c1@+ union :: c -> c -> c+ -- | @c0 `subsumes` c1@ if @c0@ permits all orderings permited by @c1@ , subsumes :: c -> c -> m Bool+ -- | @'exRefine' c t u@ strengthens constraints @c@ to permit the rewrite step+ -- from @t@ to @u@. This is used to determine if considering term @u@ by rewriting+ -- from @t@ would permit more rewrite applications.+ , exRefine :: c -> term -> term -> c } --- A mapping of terms, to the rewritten terms that need to be fully explored--- in order for this term to be fully explored+-- | A mapping of terms, to the rewritten terms that need to be fully explored+-- | in order for this term to be fully explored data ExploredTerms term c m =- ET (M.HashMap term (c, (S.HashSet term))) (ExploreFuncs c m) ExploreStrategy---- trace' = trace-trace' _ x = x-+ ET (M.HashMap term (c, S.HashSet term)) (ExploreFuncs term c m) ExploreStrategy 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 term 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 insert :: (Eq term, Hashable term) => term -> c -> S.HashSet term -> ExploredTerms term c m -> ExploredTerms term c m-insert t oc s (ET etMap ef@(EF union _ ) strategy) = ET (M.insertWith go t (oc, s) etMap) ef strategy+insert t oc s (ET etMap ef@(EF union _ _) strategy) = ET (M.insertWith go t (oc, s) etMap) ef strategy where- go (oc1, s1) (oc2, s2) = (union oc1 oc2, S.union s1 s2)+ go (oc1, s1) (oc2, s2) = (oc1 `union` oc2, S.union s1 s2) -lookup :: (Eq term, Hashable term) => term -> ExploredTerms term c m -> Maybe (c, (S.HashSet term))+lookup :: (Eq term, Hashable term) => term -> ExploredTerms term c m -> Maybe (c, S.HashSet term) lookup t (ET etMap _ _) = M.lookup t etMap -isFullyExplored :: forall term c m . (Monad m, Show term, Eq term, Hashable term, Eq c) =>+-- | @isFullyExplored t c M = not explorable(t, c)@ where @explorable@ is+-- defined as in the REST paper. Also incorporates an optimization described+-- here: https://github.com/zgrannan/rest/issues/9+isFullyExplored :: forall term c m . (Monad m, Eq term, Hashable term, Hashable c, Eq c, Show c) => term -> c -> ExploredTerms term c m -> m Bool-isFullyExplored t0 oc0 et@(ET _ (EF{subsumes}) _) = result where+isFullyExplored t0 oc0 et@(ET _ (EF{subsumes,exRefine}) _) = result where - result = go S.empty [t0]- -- if (trace ("Check " ++ show t0) go) S.empty [t0]- -- then trace (show t0 ++ " is fully explored.") True- -- else False+ result = go S.empty [(t0, oc0)] - go :: S.HashSet term -> [term] -> m Bool+ -- Arg 1: Steps that have already been seen+ -- Arg 2: Steps to consider+ go :: S.HashSet (term, c) -> [(term, c)] -> m Bool++ -- Completed worklist, this term is fully explored at these constraints go _ [] = return True- go seen (h:t) | Just (oc, trms) <- lookup h et++ -- Term `h` has been seen before at constraints `oc`+ go seen ((h, oc'):rest) | Just (oc, trms) <- lookup h et = do- ns <- oc `subsumes` oc0- if ns- then go seen' t+ exploringPathWouldNotPermitDifferentSteps <- oc `subsumes` oc'+ if exploringPathWouldNotPermitDifferentSteps+ then go seen' rest else- let ts = (S.union trms (S.fromList t)) `S.difference` seen'- in go seen' (S.toList ts)+ let+ -- Exploring `h` at these constraints+ -- would allow exploration of each t in trms,+ -- at the constraints generated by the step from h to t+ trms' = S.map (\t -> (t, exRefine oc' h t)) trms+ ts = S.union trms' (S.fromList rest) `S.difference` seen'+ in+ go seen' (S.toList ts) where- seen' = S.insert h seen+ seen' = S.insert (h, oc') seen - go _ _ | otherwise = trace' "GF" $ return False -- trace ("Must check " ++ show t0 ++ " . Visited: " ++ (show $ visited t0 et)) False+ -- There exists a reachable term that has never previously been seen; not fully explored+ go _ _ = return False -shouldExplore :: forall term c m . (Monad m, Show term, Eq term, Hashable term, Eq c, Show c) =>+-- | @'shouldExplore' t c et@ determines if rewrites originating from term @t@ at+-- constraints @c@ should be considered, given the already explored terms of @et@+-- and the associated 'ExploreStrategy'+shouldExplore :: forall term c m . (Monad m, Eq term, Hashable term, Eq c, Show c, Hashable c) => term -> c -> ExploredTerms term c m -> m Bool shouldExplore t oc et@(ET _ EF{subsumes} strategy) = case strategy of@@ -87,7 +120,5 @@ case lookup t et of Just (oc', _) -> do s <- oc' `subsumes` oc- return $ if s- then trace' ((show oc') ++ " subsumes " ++ (show oc)) False- else True+ return $ not s Nothing -> return True
+ src/Language/REST/Internal/EquivalenceClass.hs view
@@ -0,0 +1,81 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE StandaloneDeriving #-}++module Language.REST.Internal.EquivalenceClass+ ( isMember+ , isSingleton+ , insert+ , union+ , singleton+ , fromList+ , toList+ , head+ , EquivalenceClass+ , elems+ , 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)++-- | Equivalent classes of the @(==)@ relation of a type @a@.+newtype EquivalenceClass a =+ -- | The set contains all of the elements of the class+ EquivalenceClass (S.Set a)+#if MIN_VERSION_hashable(1,3,5)+ deriving (Ord, Eq, Generic, Hashable)+#else+ deriving (Ord, Eq, Generic)+#endif++#if !MIN_VERSION_hashable(1,3,5)+deriving instance Hashable (S.Set a) => Hashable (EquivalenceClass a)+#endif++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++{-# INLINE elems #-}+elems :: EquivalenceClass a -> S.Set a+elems (EquivalenceClass ec) = ec
+ src/Language/REST/Internal/ListT.hs view
@@ -0,0 +1,43 @@+-- | Defines a version of the ListT monad transformer, used in the REST search++module Language.REST.Internal.ListT where++import Control.Applicative+import Control.Monad.Trans++newtype ListT m a = ListT {+ runListT :: m [a]+}++instance (Monad m) => Functor (ListT m) where+ fmap f (ListT mxs) = ListT $ do+ map f <$> mxs++instance (Monad m) => Applicative (ListT m) where+ pure x = ListT (return [x])+ (ListT mf) <*> (ListT mx) = ListT $ do+ fs <- mf+ xs <- mx+ return $ do+ f <- fs+ map f xs++instance (Monad m) => Monad (ListT m) where+ return x = ListT (return [x])+ (ListT mxs) >>= f = ListT $ do+ xs <- mxs+ res <- mapM (runListT . f) xs+ return $ concat res++instance (Monad m) => Alternative (ListT m) where+ empty = ListT (return [])+ (ListT mxs) <|> (ListT mys) = ListT $ do+ xs <- mxs+ if not $ null xs+ then mxs+ else mys++instance MonadTrans ListT where+ lift mx = ListT $ do+ x <- mx+ return [x]
+ src/Language/REST/Internal/MultiSet.hs view
@@ -0,0 +1,87 @@+{-# 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++newtype 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 k m@ removes a single instance of @k@ from the multiset @m.+-- If @k is not in the multiset, the original multiset is returned+delete :: (Hashable a, Eq a) => a -> MultiSet a -> MultiSet a+delete k = deleteMany k 1++-- | @delete k n m@ removes @n@ instances of @k@ from the multiset @m@.+-- If there are less than @n@ instances of @k@ in the multiset, all+-- instances are removed.+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) = 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 k m@ returns @true@ iff there is at least one instance of @k@+-- in @m@+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) = replicate num 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)+ = 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
+ src/Language/REST/Internal/MultisetOrder.hs view
@@ -0,0 +1,85 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveAnyClass #-}++-- | This module defines a constraint generator for a multiset+-- quasi-ordering. For more details, please see the definition+-- of @mul@ in section 4.2.1 of the paper.+module Language.REST.Internal.MultisetOrder (multisetOrder) 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 = go (M.toList ts0) M.empty 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 = 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 (`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))+++-- | Given a [constraint generator]("Language.REST.WQOConstraints#t:ConstraintGen") @cgen@ that generates constraints a WQO on+-- @base@ implied by a relation between elements of @lifted@, @'multisetOrder' cgen@+-- yields a constraint generator on elements of base implied by a relation between+-- multisets of @lifted@.+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')
+ src/Language/REST/Internal/OpOrdering.hs view
@@ -0,0 +1,97 @@+++{-# LANGUAGE FlexibleInstances #-}+++-- | This module defines an interface for 'WQO's on 'Op'erators,+-- for example, that are used as the precedence for an [RPQO]("Language.REST.RPO").+module Language.REST.Internal.OpOrdering (+ empty+ , OpOrdering+ , 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 o f g@ returns @true@ if @f > g@ in @o@+opGT :: OpOrdering -> Op -> Op -> Bool+opGT s f g = getRelation s f g == Just QGT++-- | @opEQ o f g@ returns @true@ if @f = g@ in @o@+opEQ :: OpOrdering -> Op -> Op -> Bool+opEQ s f g = getRelation s f g == Just QEQ++-- | @f >. g@ generates a new ordering with @f@ greater than @g@.+-- This function is undefined if f == g.+(>.) :: Op -> Op -> OpOrdering+(>.) f g = fromJust $ WQO.singleton (f, g, QGT)++-- | @f =. g@ generates a new ordering with @f@ equal to @g@.+-- This function is undefined if f == g.+(=.) :: Op -> Op -> OpOrdering+(=.) f g = fromJust $ WQO.singleton (f, g, QEQ)++-- | @f <. g@ generates a new ordering with @f@ less than @g@.+-- This function is undefined if f == g.+(<.) :: Op -> Op -> OpOrdering+(<.) f g = g >. f++-- | @parseOO str@ returns the ordering defined by @str@. If the input describes+-- /any/ ordering, (i.e "f = f"), then this function returns 'Nothing'.+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 '*'))
+ src/Language/REST/Internal/Orphans.hs view
@@ -0,0 +1,34 @@+{-# LANGUAGE CPP #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}++module Language.REST.Internal.Orphans() where++#if !MIN_VERSION_hashable(1,3,4)+import Data.Hashable+import Data.Hashable.Lifted+import Data.Set as Set+import Data.Map as Map++instance Hashable1 Set where+ liftHashWithSalt h s x = Set.foldl' h (hashWithSalt s (Set.size x)) x++instance (Hashable a) => Hashable (Set a) where+ hashWithSalt = hashWithSalt1++instance Hashable2 Map.Map where+ liftHashWithSalt2 hk hv s m = Map.foldlWithKey'+ (\s' k v -> hv (hk s' k) v)+ (hashWithSalt s (Map.size m))+ m++instance Hashable k => Hashable1 (Map.Map k) where+ liftHashWithSalt h s m = Map.foldlWithKey'+ (\s' k v -> h (hashWithSalt s' k) v)+ (hashWithSalt s (Map.size m))+ m++-- | @since 1.3.4.0+instance (Hashable k, Hashable v) => Hashable (Map.Map k v) where+ hashWithSalt = hashWithSalt2++#endif
+ src/Language/REST/Internal/PartialOrder.hs view
@@ -0,0 +1,139 @@+{-# 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 Language.REST.Internal.Orphans ()+import Text.Printf++-- | Irreflexive (strict) partial orders+newtype PartialOrder a =+ -- | @PartialOrder m@ represents the relation+ --+ -- > (>) = { (a, b) | (a, bs) <- toList m, b <- bs }+ --+ -- Transitivity implies that @m ! a == { b | a > b}@ if @a@ is in the map.+ --+ -- Asymmetry implies that @member a (m ! b)@ implies+ -- @not (member b (m ! a))@.+ --+ -- Irreflexivity means that @a@ cannot be in @m ! 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 (>) a b@ iff @a /= b && not (a > b) && not (b > a)@+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 (>) a b == (a > b)@+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 a (>) = { b | b > a }+ascendants :: Ord k => k -> PartialOrder k -> S.Set k+ascendants k (PartialOrder m) = M.keysSet $ M.filter (S.member k) m++-- | descendents a (>) = { b | a > b }+descendents :: Ord a => a -> PartialOrder a -> S.Set a+descendents k (PartialOrder m) = M.findWithDefault S.empty k m++-- | @insertUnsafe (>) a b@ is unsafe because it may not respect some+-- of its properties if @canInsert (>) a b@ doesn't hold.+{-# 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 = 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 olds new (>)@ replaces every element in @olds@ with+-- @new@ in the partial order @(>)@.+--+-- More formally:+--+-- > replaceUnsafe olds new (>) =+-- > { (a, b) | notElem a olds, notElem b olds }+-- > U { (new, b) | o <- olds, o > b }+-- > U { (a, new) | o <- olds, a > o }+--+-- This operation is unsafe because it only yields a partial order+-- if forall @o@ in @olds@:+-- * @o > b@ implies @not (b > new)@, and+-- * @a > o@ implies @not (new > a)@.+--+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 _ -> k `notElem` 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 = s++ hasFrom set = any (`S.member` set) froms
+ src/Language/REST/Internal/Rewrite.hs view
@@ -0,0 +1,75 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}++module Language.REST.Internal.Rewrite+ ( Rewrite(..)+ , Subst+ , named+ , subst+ , unify+ ) where++import GHC.Generics (Generic)++import Data.Maybe (isNothing)+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+++-- | @Rewrite t u s@ defines a rewrite rule \( t \rightarrow u \), with+-- an optional name @s@.+data Rewrite = Rewrite MetaTerm MetaTerm (Maybe String)+ deriving (Eq, Ord, Generic, Hashable, Show)++-- | 'Subst' is a mapping from variable names to 'RuntimeTerm's.+-- Normally this would be generated by unifying the left-hand-side of+-- a 'Rewrite' with a term.+type Subst = M.HashMap String RuntimeTerm++-- | @named r n@ assigns the name @n@ to rule @r@, replacing any+-- existing name+named :: Rewrite -> String -> Rewrite+named (Rewrite t u _) n = Rewrite t u (Just n)++-- | @subst s m@ replaces the variables in the 'MetaTerm' @m@ with 'RuntimeTerm's+-- in the substitution 's'. This function returns an error if any variables in 'm'+-- do not have a substituion+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 m r su@ extends the substitution @su@ to generate a new+-- substitution that unifies @m@ and @r@. Returns 'Nothing' if su+-- cannot be extended to unify the terms.+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 | isNothing (M.lookup s su)+ = 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 _ = S.empty
+ src/Language/REST/Internal/Util.hs view
@@ -0,0 +1,15 @@+module Language.REST.Internal.Util where++import qualified Data.List as L++-- | @removeEqBy f xs ys@ removes elements from @xs@ and @ys@ such that for each+-- element x removed from xs, an element y is removed from ys such @f x y@.+-- In other words in the result @(xs', ys')@, there does not exist any @x@ in+-- @xs'@, @y@ in @ys'@ such that @f x y@.+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')
+ src/Language/REST/Internal/WQO.hs view
@@ -0,0 +1,358 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}++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.Internal.Orphans ()+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++-- | Well-founded reflexive partial orders+data WQO a =+ -- Invariant: the first set contains all equivalence classes+ --+ -- The strict partial order describes the ordering of the+ -- equivalence classes in the first set.+ 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' =+ [show po | not (PO.isEmpty 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 = insertMaybe empty++{-# INLINE elems #-}+elems :: (Ord a) => WQO a -> S.Set a+elems (WQO ec _) = S.unions $ map EC.elems (S.toList ec)++-- | @getEquivalenceClasses (>=) a b@ retrieves the equivanlence classes of+-- @a@ and @b@.+--+-- TODO: Why are these looked up in pairs and not individually?+{-# 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++-- | Like @getEquivalenceClasses@ but only yields a result+-- if classes of equivalence are found for both elements.+{-# 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++-- | @getRelation (>=) a b == QEQ@ iff @a >= b@+-- @getRelation (>=) a b == QGT@ iff @a > b@+{-# 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 (>=) ec x@ adds an element @x@ to the equivalence class+-- @ec@ of @(>=)@.+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 (>=) ec1 ec2@ combines the equivalence classes @ec1@ and @ec2@+-- of @(>=)@.+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 #-}+-- | @w1 `notStrongerThan` w2@ if it is possible to extend @w1@ with additional+-- relations to obtain @w2@+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 =+ 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+ zipWith (\ a b -> (a, b, QEQ)) 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 wqo as bs@ returns a new WQO that contains only the necessary+-- relations to relate elements from @as@ with elements in @bs@ as they are+-- related in @wqo@.+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) = 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)++-- | Generates all the possible orderings of the elements in the given set.+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')
+ src/Language/REST/Internal/WorkStrategy.hs view
@@ -0,0 +1,39 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+module Language.REST.Internal.WorkStrategy (+ GetWork,+ WorkStrategy(..),+ bfs,+ notVisitedFirst) where++import Language.REST.ExploredTerms as ET+import Language.REST.Path++import Data.Hashable+import qualified Data.List as L++type GetWork m rule term oc = [Path rule term oc] -> ExploredTerms term oc m -> (Path rule term oc, [Path rule term oc])++-- | 'WorkStrategy' defines the procedure for choosing which pending path REST explores+newtype WorkStrategy rule term oc = WorkStrategy (forall m . GetWork m rule term oc)++-- | Explore the rewrite tree in BFS style. Using this strategy enables finding the+-- shortest rewrite path to a desired term.+bfs :: WorkStrategy rule term oc+bfs = WorkStrategy bfs'++-- | Prioritize searching for terms that haven't been seen before. This strategy may+-- explore all reachable terms earlier, reducing the need to explore down the remaining+-- unexplored paths.+notVisitedFirst :: (Eq term, Eq rule, Eq oc, Hashable term) => WorkStrategy rule term oc+notVisitedFirst = WorkStrategy notVisitedFirst'++bfs' :: [Path rule term oc] -> 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, Hashable term) => GetWork m rule term oc+notVisitedFirst' paths et =+ case L.find (\p -> not (ET.visited (runtimeTerm p) et)) paths of+ Just p -> (p, L.delete p paths)+ Nothing -> (head paths, tail paths)
+ src/Language/REST/KBO.hs view
@@ -0,0 +1,50 @@+{-# 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 t u@ returns the SMT expression describing constraints+-- on the weights of function symbols such that @t@ is greater than @u@+-- in the KBO ordering.+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)+++-- | OCA for a quasi-order extension to the Knuth-Bendix ordering+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)
+ src/Language/REST/LPO.hs view
@@ -0,0 +1,92 @@+++{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+++++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 = zipWith (lpo' False oc EQ cs') 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 = [singleton oc (f =. g) | f /= g]+++ tDominatesUs = intersectAll oc (map go us) where+ go = lpo' strict oc GT cs t+++-- | Constraint generator for a quasi-order extension to the Lexicographic path ordering+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++-- | Constraint generator for a strict version of the quasi-order extension to+-- the Lexicographic path ordering.+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
src/Language/REST/MetaTerm.hs view
@@ -6,11 +6,11 @@ import Data.String import Data.Hashable import GHC.Generics (Generic)-import qualified Data.Set as S import Language.REST.Op import Language.REST.RuntimeTerm +-- | A MetaTerm is a term with variables; used for 'Rewrite' rules data MetaTerm = Var String | RWApp Op [MetaTerm] deriving (Eq, Ord, Show, Generic, Hashable)@@ -18,6 +18,7 @@ instance IsString MetaTerm where fromString = Var +-- | Helper class, enabling conversion of 'RuntimeTerm's to 'MetaTerm's class ToMetaTerm a where toMetaTerm :: a -> MetaTerm @@ -26,9 +27,3 @@ instance ToMetaTerm RuntimeTerm where toMetaTerm (App f xs) = RWApp f (map toMetaTerm xs)--termOps :: ToMetaTerm a => a -> S.Set Op-termOps = go . toMetaTerm where- go :: MetaTerm -> S.Set Op- go (Var _) = S.empty- go (RWApp op trms) = S.insert op (S.unions (map go trms))
− src/Language/REST/MultiSet.hs
@@ -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
− src/Language/REST/MultisetOrder.hs
@@ -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'))
+ src/Language/REST/OCAlgebra.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+module Language.REST.OCAlgebra where++-- | The "Ordering Constraint Algebra", as described in section 4.2 of the paper.+-- @OCAlgebra c a m@ is an OCA with language of constraints @c@, applied to terms+-- of type @a@. @m@ is the computation context for @isSat@.+data OCAlgebra c a m = OCAlgebra+ { isSat :: c -> m Bool -- ^ Checks if the constraints are satisfiable+ , refine :: c -> a -> a -> c -- ^ @refine c t u@ strengthens @c@ to permit @t >= u@+ , top :: c -- ^ Initial constraints for use in REST++ , union :: c -> c -> c -- ^ Computes the union of constraints; used in 'ExploredTerms' as an optimization+ -- A safe default implementation is @union c1 c2 = c2@++ , notStrongerThan :: c -> c -> m Bool -- ^ @c1 `notStrongerThan c2@ if @c1@ permits all orderings allowed by @c2@+ -- A safe default implementation is @notStrongerThan _ _ = return false@+ }++-- | @fuelOC n@ is an OCA that permits @n@ rewrite steps+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' = max+ notStrongerThan' c c' = return $ c >= c'++-- | @contramap f oca@ transforms an OCA of terms of type @a@ terms of type @b@,+-- by using @f@ to convert terms of @b@ to equivalent ones of @a@+contramap :: forall c a b m .+ (b -> a)+ -> OCAlgebra c a m+ -> OCAlgebra c b m+contramap f oca = oca{refine = refine'}+ where+ refine' :: c -> b -> b -> c+ refine' c t1 t2 = refine oca c (f t1) (f t2)++-- | @bimapConstraints to from oca@ yields an oca using @d@ to track constraints; @to@ and @from@ should+-- define an isomorphism between c and d+bimapConstraints :: forall c d a m .+ (c -> d)+ -> (d -> c)+ -> OCAlgebra c a m+ -> OCAlgebra d a m+bimapConstraints to from oca = OCAlgebra isSat' refine' (to (top oca)) union' notStrongerThan'+ where+ isSat' :: d -> m Bool+ isSat' c = isSat oca (from c)++ refine' :: d -> a -> a -> d+ refine' c t1 t2 = to $ refine oca (from c) t1 t2++ union' :: d -> d -> d+ union' c1 c2 = to $ union oca (from c1) (from c2)++ notStrongerThan' :: d -> d -> m Bool+ notStrongerThan' c1 c2 = notStrongerThan oca (from c1) (from c2)
src/Language/REST/OCToAbstract.hs view
@@ -1,5 +1,4 @@ {-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE ImplicitParams #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -7,24 +6,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--showHash :: Show a => a -> String-showHash = show . hash . show+import Language.REST.SMT (ToSMTVar) +-- | @lift@ takes a representation of constraints on a WQO over @base@,+-- alongside a function used to generate constraints to permit a relation on terms @lifted@,+-- and returns the corresponding Ordering Constraints Algebra 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'@@ -33,7 +31,7 @@ } where isSat' :: impl base -> m Bool- isSat' aoc = OC.isSatisfiable oc aoc+ isSat' = OC.isSatisfiable oc top' :: impl base top' = OC.noConstraints oc@@ -41,13 +39,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
src/Language/REST/Op.hs view
@@ -9,9 +9,9 @@ import Data.Hashable import Data.String import GHC.Generics (Generic)-import Data.Text import Language.REST.SMT +-- | The operators used in 'RuntimeTerm' and 'MetaTerm' newtype Op = Op Text deriving (Eq, Ord, Hashable, Generic) instance Show Op where@@ -38,4 +38,6 @@ go ' ' = "_space_" go '∪' = "_cup_" go '\\' = "_bslash_"+ go '(' = "_lp_"+ go ')' = "_rp_" go c = singleton c
− src/Language/REST/OpOrdering.hs
@@ -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 '*'))
− src/Language/REST/OrderingConstraints.hs
@@ -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
− src/Language/REST/OrderingConstraints/ADT.hs
@@ -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
− src/Language/REST/OrderingConstraints/Lazy.hs
@@ -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
− src/Language/REST/OrderingConstraints/Strict.hs
@@ -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
− src/Language/REST/PartialOrder.hs
@@ -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
src/Language/REST/Path.hs view
@@ -7,27 +7,34 @@ import qualified Data.HashSet as S import GHC.Generics (Generic) import Data.Hashable-import Language.REST.Types +-- | @Step@ represents an intermediate step in a 'Path' explored by REST data Step rule term a = Step {- term :: PathTerm rule term- , rule :: rule- , ordering :: a- , fromPLE :: Bool+ term :: PathTerm rule term -- ^ The "from" term in this path+ , rule :: rule -- ^ The rule generating the next term+ , ordering :: a -- ^ The generated constraints from applying the rule+ , fromPLE :: Bool -- ^ Whether the term was derived from a provably terminating eval function } deriving (Eq, Ord, Generic, Hashable) +-- | @PathTerm@ is the term explored at a path data PathTerm rule term = PathTerm { pathTerm :: term+ , rejected :: S.HashSet (term, rule) -- ^ The orderings FROM pathTerm that were rejected.+ -- TODO: This should be removed, as it's really only used+ -- in the visualization - -- The orderings FROM pathTerm that were rejected- , rejected :: S.HashSet (term, rule) } deriving (Eq, Ord, Generic, Hashable) +-- | A path explored by REST.+-- The head of the 1st part of the tuple is the initial term.+-- The 2nd part of the tuple is the last term. type Path rule term a = ([Step rule term a], PathTerm rule term) +-- | Extracts the list of terms from the path pathTerms :: Path rule term a -> [term] pathTerms (xs, x) = map pathTerm $ map term xs ++ [x] +-- | Extracts the last (most recently generated) term runtimeTerm :: Path rule term a -> term runtimeTerm (_, pt) = pathTerm pt
− src/Language/REST/ProofGen.hs
@@ -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
src/Language/REST/RESTDot.hs view
@@ -1,7 +1,15 @@+{-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}-module Language.REST.RESTDot where +-- | This module is responsible for rendering GraphViz graphs corresponding to an+-- execution of the REST algorithm.+module Language.REST.RESTDot (+ PrettyPrinter(..)+ , ShowRejectsOpt(..)+ , writeDot+ ) where+ import Data.List import Data.Hashable import qualified Data.Set as S@@ -9,13 +17,20 @@ import Language.REST.Dot import Language.REST.Path-import Language.REST.Types +-- | Controls how rejected paths should be visualized+data ShowRejectsOpt =+ ShowRejectsWithRule -- ^ Display rejected paths, and the rule that generated them+ | ShowRejectsWithoutRule -- ^ Display rejected paths, but don't display the rule that generated them+ | HideRejects -- ^ Do not show rejected paths+ deriving Eq++-- | Controls how rules, terms, orderings, and rejected paths should be displayed data PrettyPrinter rule term ord = PrettyPrinter { printRule :: rule -> String , printTerm :: term -> String , printOrd :: ord -> String- , showRejects :: Bool+ , showRejects :: ShowRejectsOpt } rejNodeID :: (Hashable rule, Hashable term, Hashable a) => GraphType -> Path rule term a -> term -> String@@ -23,11 +38,11 @@ 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 _ pp _ | showRejects pp == HideRejects = S.empty+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,13 +56,13 @@ => 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-toEdges gt pp path = allRej `S.union` (S.fromList $ map toEdge (zip subs (tail subs)))+toEdges gt pp path = allRej `S.union` S.fromList (zipWith (curry toEdge) subs (tail subs)) where subs = subPaths path @@ -55,29 +70,33 @@ rejEdges :: Path rule term a -> S.Set Edge rejEdges p@(_, PathTerm _ rej) =- if showRejects pp+ if showRejects pp /= HideRejects 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"+ ruleText r =+ if showRejects pp == ShowRejectsWithRule+ then printRule pp r+ else ""+ go (rejTerm, r) =+ Edge (nodeID (endNode gt pp p)) (rejNodeID gt p rejTerm) (ruleText r) "red" " " "dotted" toEdge :: (Path rule term a, Path rule term a) -> Edge toEdge (p0, p1@(ts, _)) = let step = last ts- color = if (fromPLE step) then "brown" else "darkgreen"- subLabel = printOrd pp (ordering step)+ color = if fromPLE step then "brown" else "darkgreen"+ 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 =@@ -94,6 +113,7 @@ unions :: (Ord a, Eq a, Hashable a) => S.Set (S.Set a) -> S.Set a unions = S.unions . S.toList +-- | @writeDot name gt printer paths@ generates a graphViz graph from @paths@ with name @name@. writeDot :: (Hashable rule, Hashable term, Ord a, Hashable a) => String -> GraphType -> PrettyPrinter rule term a -> S.Set (Path rule term a) -> IO () writeDot name gt printer paths = mkGraph name (toGraph gt printer paths)
src/Language/REST/RPO.hs view
@@ -3,35 +3,29 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ImplicitParams #-} -module Language.REST.RPO (rpo, rpoTerm, rpoGTE, rpoGTE', synGTE) where+-- | This module contains the implementation of the Recursive Path Quasi-Ordering,+-- defined in section 4.2.1 of the REST paper+module Language.REST.RPO (rpo, 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,20 +36,17 @@ 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 CacheKey oc = (oc Op, Relation, RuntimeTerm, RuntimeTerm) type Cache oc = M.HashMap (CacheKey oc) (oc Op) @@ -76,19 +67,17 @@ 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 -+-- | The constraint generator for RPQO. That is, given terms @t@, @u@, @rpo@ generates+-- the constraints on n RPQO ≥ᵣ such that t ≥ᵣ u. 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,41 +89,39 @@ 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)- 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)- ]--+ cs' = noConstraints oc+ result = cached (cs, r, t, u) (intersect oc cs <$> result')+ 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 t u@ generates the constraints a WQO over 'Op' (via @impl@) that ensures+-- that t ≥ᵣ u in the result RPQO ≥ᵣ.+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' impl oc t u = rpo impl GTE oc 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 = rpo impl GTE -- Non symbolic version@@ -142,19 +129,13 @@ 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')-+-- | Performs the (concrete) RPQO calculation. @synGTE o t u@ returns+-- true iff t ≥ᵣ u using an RPQO with precedence @o@. 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 +147,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'
src/Language/REST/Rest.hs view
@@ -1,108 +1,119 @@-{-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE DeriveAnyClass #-}++ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE ImplicitParams #-}+ {-# LANGUAGE NamedFieldPuns #-}+{-# OPTIONS_GHC -Wno-error=deprecations #-} +-- | This module contains the core REST algorithm module Language.REST.Rest ( rest , pathsResult , termsResult- , terms , PathsResult(..)+ , TermsResult , WorkStrategy(..) , RESTParams(..)+ , RESTResult(..) ) where import Control.Monad-import Control.Monad.List+import Control.Monad.Trans import Data.Hashable import qualified Data.HashSet as S 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.ListT+import Language.REST.Internal.WorkStrategy +-- | The set of all 'Path's explored by REST. newtype PathsResult rule term oc = PathsResult (S.HashSet (Path rule term oc)) +-- | The set of all terms explored by REST. newtype TermsResult rule term oc = TermsResult (S.HashSet term) +-- | An initial (empty) instance of 'PathsResult'+pathsResult :: PathsResult rule term oc pathsResult = PathsResult S.empty++-- | An initial (empty) instance of 'TermsResult'+termsResult :: TermsResult rule term oc termsResult = TermsResult S.empty +-- | This class encapsulates the mechanism for REST to store the result of its computation.+-- For example, we include two instances: 'PathsResult', which stores each 'Path' generated+-- by REST (useful for debugging and visualization); and 'TermsResult', which only stores the+-- resulting terms (which uses less memory and is likely more performant). class RESTResult a where+ -- | Includes a term in the result includeInResult :: (Hashable oc, Eq oc, Hashable rule, Eq rule, Hashable term, Eq term) => Path rule term oc -> a rule term oc -> a rule term oc- terms :: (Eq term, Hashable term) => a rule term oc -> S.HashSet term+ -- | Obtains the terms explored by REST+ resultTerms :: (Eq term, Hashable term) => a rule term oc -> S.HashSet term instance RESTResult PathsResult where includeInResult p (PathsResult s) = PathsResult (S.insert p s)- terms (PathsResult s) = S.fromList (concatMap pathTerms $ S.toList s)-+ resultTerms (PathsResult s) = S.fromList (concatMap pathTerms $ S.toList s) instance RESTResult TermsResult where includeInResult p (TermsResult s) = TermsResult (S.union s (S.fromList $ pathTerms p))- terms (TermsResult s) = s+ resultTerms (TermsResult s) = s data RESTState m rule term oc et rtype = RESTState { finished :: rtype rule term oc , working :: [Path rule term oc]- , explored :: ExploredTerms et oc m+ , explored :: ExploredTerms term oc m , targetPath :: Maybe (Path rule term oc) } -data RESTParams m rule term oc et rtype = RESTParams+data RESTParams m rule term oc rtype = RESTParams { re :: S.HashSet rule , ru :: S.HashSet rule- , toET :: term -> et , target :: Maybe term- , workStrategy :: WorkStrategy rule term et oc- , ocImpl :: AbstractOC oc term m+ , workStrategy :: WorkStrategy rule term oc+ , ocImpl :: OCAlgebra oc term m , initRes :: rtype rule term oc+ , etStrategy :: ExploreStrategy } -rest :: forall m rule term oc et rtype .+-- @rest params terms@ performs the REST search from initial term @term@ with parameters@params@.+rest :: forall m rule term oc rtype . ( MonadIO m , RewriteRule m rule term- , Show et , Hashable term , Eq term , Hashable rule- , Hashable et , Hashable oc , Eq rule- , Eq et , Eq oc , Show oc , RESTResult rtype)- => RESTParams m rule term oc et rtype+ => RESTParams m rule term oc rtype -> term- -> m ((rtype rule term oc), Maybe (Path rule term oc))-rest RESTParams{re,ru,toET,ocImpl,workStrategy,initRes,target} t =+ -> m (rtype rule term oc, Maybe (Path rule term oc))+rest RESTParams{re,ru,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) (refine ocImpl)) etStrategy rest' (RESTState fin [] _ targetPath) = return (fin, targetPath) rest' state@(RESTState _ paths et (Just targetPath))- | ((steps, _), remaining) <- ws paths toET et+ | ((steps, _), remaining) <- ws paths et , 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 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 +121,7 @@ rest' (state{ working = remaining }) where - (path@(ts, PathTerm t _), remaining) = ws paths toET et+ (path@(ts, PathTerm ptTerm _), remaining) = ws paths et lastOrdering :: oc lastOrdering = if L.null ts then top ocImpl else ordering $ last ts@@ -127,14 +138,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+ 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))@@ -151,11 +162,11 @@ , finished = if null p' then includeInResult (ts, pt) fin else fin , explored = let- deps = S.map (toET . fst) (S.union evalRWs userRWs)+ deps = S.map fst (S.union evalRWs userRWs) in- ET.insert (toET t) lastOrdering deps et+ ET.insert 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 +175,7 @@ } - pt = PathTerm t rejectedUserRewrites+ pt = PathTerm ptTerm rejectedUserRewrites rejectedUserRewrites :: S.HashSet (term, rule) rejectedUserRewrites = S.fromList $ do@@ -177,12 +188,12 @@ evalPaths = runListT $ do (t', r) <- ListT $ return (S.toList evalRWs) guard $ L.notElem t' tsTerms- let ord = refine ocImpl lastOrdering t t'- lift (shouldExplore (toET t') ord et) >>= guard+ let ord = refine ocImpl lastOrdering ptTerm t'+ lift (shouldExplore t' ord et) >>= guard return (ts ++ [Step pt r ord True], PathTerm t' S.empty) userPaths = runListT $ do (t', r) <- liftSet userRWs ord <- ListT $ return $ Mb.maybeToList $ M.lookup t' acceptedUserRewrites- lift (shouldExplore (toET t') ord et) >>= guard+ lift (shouldExplore t' ord et) >>= guard return (ts ++ [Step pt r ord False], PathTerm t' S.empty)
− src/Language/REST/Rewrite.hs
@@ -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
src/Language/REST/RewriteRule.hs view
@@ -4,5 +4,10 @@ import qualified Data.HashSet as S +-- | A class for datatypes that can be used as rewrite rules class RewriteRule m rule term where+ -- | @apply term rule@ returns the set of resulting terms that can be generated+ -- from @term@ using @rule@. Multiple terms are possible if the rule applies to+ -- multiple subterms. The result is embedded in a computation context @m@;+ -- this enables support for SMT-based conditional rewriting, for example. apply :: term -> rule -> m (S.HashSet term)
src/Language/REST/RuntimeTerm.hs view
@@ -1,7 +1,13 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveAnyClass #-} -module Language.REST.RuntimeTerm where+module Language.REST.RuntimeTerm+ ( RuntimeTerm(..)+ , ToRuntimeTerm(..)+ , subTerms+ , contains+ )+where import Data.Hashable import GHC.Generics (Generic)@@ -10,12 +16,14 @@ import Language.REST.Op +-- | Ground terms data RuntimeTerm = App Op [RuntimeTerm] deriving (Eq, Ord, Generic, Hashable) instance Show RuntimeTerm where show (App op []) = show op show (App op ts) = printf "%s(%s)" (show op) $ L.intercalate ", " (map show ts) +-- | Transformable to a ground term class ToRuntimeTerm a where toRuntimeTerm :: a -> RuntimeTerm @@ -25,15 +33,26 @@ instance ToRuntimeTerm RuntimeTerm where toRuntimeTerm = id -subTerms :: RuntimeTerm -> [(RuntimeTerm, (RuntimeTerm -> RuntimeTerm))]+-- | @subTerms t@ returns a list of pairs @(s, f)@, where @s@ is a subterm of @t@,+-- and @f@ is a function that takes a replacement @s'@ for @s@, and generates a new+-- term where @s@ is replaced with @s'@ in @t@. Also includes the pair (t, id),+-- representing the term itself.+-- TODO: Consider more efficient implementations+subTerms :: RuntimeTerm -> [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)] subTerms t@(App f ts) = (t, id) : concatMap st [0..length ts - 1] where- st :: Int -> [(RuntimeTerm, (RuntimeTerm -> RuntimeTerm))]+ 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)+++-- | @t `contains` u@ iff @t == u@ or @u@ is a subterm of @t@+contains :: RuntimeTerm -> RuntimeTerm -> Bool+contains t1 t2 | t1 == t2 = True+contains (App _ ts) t = any (contains t) ts
src/Language/REST/SMT.hs view
@@ -1,96 +1,273 @@ {-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GADTs #-}-{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE FunctionalDependencies #-}+ {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RankNTypes #-} -module Language.REST.SMT where+{-# LANGUAGE UndecidableInstances #-} +-- | This module contains functionality for creating SMTLIB expressions and interacting+-- with an SMT solver.+module Language.REST.SMT+ (+ checkSat+ , checkSat'+ , getModel+ , parseModel+ , killZ3+ , spawnZ3+ , smtAdd+ , smtAnd+ , smtFalse+ , smtGTE+ , smtTrue+ , withZ3+ , SolverHandle+ , SMTExpr(..)+ , SMTVar(..)+ , ToSMT(..)+ , ToSMTVar(..)+ , Z3Model+) 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)+-- | A model returned by Z3 corresponding to a satisfiable+-- set of constraints. Untyped.+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++-- | Parses Z3's model string into a 'Z3Model'.+parseModel :: String -> Z3Model+parseModel str = case parse modelParser "" str of+ Left err -> error (show err)+ Right t -> t++-- | An SMT variable+newtype SMTVar a = SMTVar T.Text deriving (Eq, Ord)++-- | SMTLib expressions 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 [] -app op trms = T.concat $ ["(", op, " ", (T.intercalate " " (map exprString trms)), ")"]+-- | Returns an SMT expression that adds all elements in the list. If the list is empty,+-- returns @Const 0@.+smtAdd :: [SMTExpr Int] -> SMTExpr Int+smtAdd [] = Const 0+smtAdd ts = Add ts +-- | `smtAnd t u` returns an smt expression representing \( t \land u \).+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 t u` returns an SMT expression \( t \geqslant u \). If @t == u@, returns 'smtTrue'.+smtGTE :: SMTExpr Int -> SMTExpr Int -> SMTExpr Bool+smtGTE t u | t == u = smtTrue+smtGTE t u = 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) +-- | The handle (stdIn, stdOut) used for interacting with Z3 type SolverHandle = (Handle, Handle) +-- | Instantiates a Z3 instance, returning the solver handle for interaction+spawnZ3 :: IO SolverHandle spawnZ3 = do (Just stdIn, Just stdOut, _, _) <- createProcess (proc "z3" ["-in"]) {std_in = CreatePipe, std_out = CreatePipe} return (stdIn, stdOut) +-- | Kills the Z3 instance by closing the standard input stream+killZ3 :: SolverHandle -> IO () killZ3 (stdIn, _) = hClose stdIn +-- | @withZ3 f@ instantiates a Z3 instance, runs @f@ with that instance,+-- and then closes the instance and returns the result+withZ3 :: MonadIO m => (SolverHandle -> m b) -> m b withZ3 f = do- z3 <- liftIO $ spawnZ3+ z3 <- liftIO spawnZ3 result <- f z3 liftIO $ killZ3 z3 return result +-- | @getModel@ instructs an instantiated SMT solver to produce its model.+getModel :: Handle -> IO ()+getModel stdIn = do+ hPutStr stdIn "(get-model)\n"+ hFlush stdIn++-- | @checkSat' handles expr@ checks satisfiability of @expr@ in an instantiated SMT solver.+-- This is wrapped in a @push@ / @pop@, so it does not change the SMT environment 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 expr@ launches Z3, to checks satisfiability of @expr@, terminating Z3+-- afterwards. Just a utility wrapper for `checkSat'` checkSat :: SMTExpr Bool -> IO Bool checkSat expr = do z3 <- spawnZ3@@ -98,11 +275,19 @@ killZ3 z3 return result +-- | This class allows elements of type @a@ to be used as SMT /vaiables/ of type @b@.+-- For example, the instance @ToSMTVar Op Int@ allows 'RuntimeTerm' operators to be+-- represented as 'Int' variables. class ToSMTVar a b | a -> b where- toSMTVar :: a -> SMTVar+ toSMTVar :: a -> SMTVar b +-- | This class allows elements of type @a@ to be used as SMT expressions of type+-- @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
src/Language/REST/Types.hs view
@@ -1,12 +1,13 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE TypeSynonymInstances #-}+ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} + module Language.REST.Types ( prettyPrint , PPArgs(..)@@ -21,17 +22,26 @@ import qualified Data.List as L import qualified Data.HashSet as S import qualified Data.Set as OS-import qualified Data.Map as M import qualified Data.Text as T import Text.Printf import Language.REST.Op import Language.REST.MetaTerm as MT-import Language.REST.RuntimeTerm as MT +-- | Arguments used for pretty-printing terms data PPArgs = PPArgs- { ppReplace :: [(T.Text, T.Text)]+ {+ -- | A list of pairs @(search, rep)@. If any operator starts with @search@+ -- for some element in the list, during the printing the operator is+ -- printed with the corresponding @rep@ in place of @search@.+ ppReplace :: [(T.Text, T.Text)]++ -- | A list of pairs @(search, rep)@. If any operator matches @search@, then it's+ -- corresponding term is printed in infix style with operator @rep@. , ppInfixOps :: [(T.Text, T.Text)]++ -- | Used to override printing for some terms. When @ppCustom m = Just s@, then @m@+ -- be printed as @s@. , ppCustom :: MetaTerm -> Maybe T.Text } @@ -40,7 +50,7 @@ replace s | Just (from, to) <- L.find ((`T.isPrefixOf` s) . fst) substs = T.append to $ T.drop (T.length from) s- replace s | otherwise = s+ replace s = s replaceAll :: MT.MetaTerm -> MT.MetaTerm replaceAll (MT.Var x) = MT.Var x@@ -50,16 +60,16 @@ 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 = go mt - needsParens (MT.RWApp (Op op) _) = op `elem` (map fst infixOps)+ needsParens (MT.RWApp (Op op) _) = op `elem` map fst infixOps needsParens _ = False data Relation = GT | GTE | EQ deriving (Eq, Generic, Hashable)@@ -69,11 +79,6 @@ show GTE = "≥" show EQ = "≅" -instance Hashable a => Hashable (OS.Set a) where- hashWithSalt i s = hashWithSalt i (OS.toList s)--instance (Hashable a, Hashable b) => Hashable (M.Map a b) where- hashWithSalt i s = hashWithSalt i (M.toList s) toOrderedSet :: (Eq a, Hashable a, Ord a) => S.HashSet a -> OS.Set a toOrderedSet = OS.fromList . S.toList
− src/Language/REST/WQO.hs
@@ -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')
+ src/Language/REST/WQOConstraints.hs view
@@ -0,0 +1,132 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE FlexibleContexts #-}++-- | This module includes a typeclass for implementations of constraints on 'WQO's+module Language.REST.WQOConstraints+ (+ WQOConstraints(..)+ , ConstraintGen+ , liftC+ , cmapConstraints+ , 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 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++-- | @WQOConstraints impl m@ defines an implementation for tracking and checking+-- satisfiability of constraints on arbitrary type @a@. Namely, instances of+-- @impl a@ are used to keep track of constraints. Satisfiability checking and+-- other computations are embedded in a computational context @m@.+data WQOConstraints impl m = OC+ {+ -- | @addConstraint wqo c@ adds constraints to @c@ to also permit the WQO @w@.+ addConstraint :: forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a++ -- | @intersect c1 c2@ returns constraints to permit only WQOs permitted by both @c1@ and+ -- @c2@. Therefore the resulting constraints are stronger (less likely to be+ -- satisifiable).+ , intersect :: forall a. (Show a, Eq a, Ord a, Hashable a) => impl a -> impl a -> impl a+ -- | @isSatisfiable c@ returns true iff @c@ permits any WQO+ , isSatisfiable :: forall a. (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => impl a -> m Bool++ -- | @c1 `notStrongerThan` c2@ iff any ordering permitted by @c1@ is also permitted+ -- by @c2@+ , notStrongerThan :: forall a. (ToSMTVar a Int, Eq a, Ord a, Hashable a) => impl a -> impl a -> m Bool+ -- | @noConstraints@ returns an instance of constraints that permits any WQO+ , 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+ -- | @c1 `union` c2@ returns constraints that permit WQOs permitted by /either/+ -- @c1@ or @c2@. The resulting constraints are therefore weaker (more likely to+ -- be satisfiable)+ , union :: forall a. (Eq a, Ord a, Hashable a) => impl a -> impl a -> impl a++ -- | @unsatisfiable@ returns an instance of constraints that does not permit any WQO+ , unsatisfiable :: forall a. impl a++ -- | @getOrdering c@ returns a concrete ordering satisfying the constraints, if one exists+ , getOrdering :: forall a. impl a -> Maybe (WQO a)+ }++-- | Returns true iff the constraints do not permit any WQO.+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++-- | Returns the constraints that permit a given WQO+singleton :: (Eq a, Ord a, Hashable a) => WQOConstraints oc m -> WQO a -> oc a+singleton OC{addConstraint, noConstraints} c = addConstraint c noConstraints++-- | Given a list of constraints @ocs@, returns constraints that permit only the WQOs+-- permitted by each @oc@ in @ocs@+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' intersect x xs++-- | Given a list of constraints @ocs@, returns constraints that permit the WQOs+-- permitted by any @oc@ in @ocs@+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' union x xs++-- | @intersectRelation oc impl (f, g, r)@ strengthens constraints represented by @impl@+-- to also ensure that @f@ and @g@ are related via relation @r@ in permitted WQOs.+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@ takes a transformation @f@ from @lifted' to lifted@, and transforms+-- a constraint generator on terms of types @lifted@ into one on terms of types @lifted'@+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 f imp@ lifts the computations of @imp@ from context @m@ to context @m'@+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)++-- @runStateConstriants initState cgen@ transforms a constraint generator in the 'State'+-- monad to one in the 'Identity' monad by using initial state @initState@'+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
+ src/Language/REST/WQOConstraints/ADT.hs view
@@ -0,0 +1,227 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE CPP #-}++#define OPTIMIZE_WQO++module Language.REST.WQOConstraints.ADT+ ( ConstraintsADT(..)+ , addConstraint+ , adtOC+ , intersect+ , union+ )+where++import GHC.Generics (Generic)++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++-- | Represents constraints over a WQO on @a@+data ConstraintsADT a =+ -- | @Sat wqo@ represents satisfiable constraints: those that permit each relation in @wqo@.+ Sat (WQO a)+ | Unsat+ -- | @Union c1 c2@ permits orderings of P1 and orderings of P2+ | Union (ConstraintsADT a) (ConstraintsADT a)+ -- | @Intersect c1 c2@ permits orderings iff permitted by P1 and permitted by P2+ | 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++-- | @intersect c1 c2@ permits orderings iff permitted by P1 and permitted by P2+intersect :: (Eq a, Ord a, Hashable a) => ConstraintsADT a -> ConstraintsADT a -> ConstraintsADT a++#ifdef OPTIMIZE_WQO+-- Optimization+intersect (Sat t) (Sat u) =+ maybe Unsat Sat (WQO.merge t u)+#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' -> Sat w' `intersect` t2+ Nothing -> Unsat+intersect (Sat w1) (Intersect t2 (Sat w2)) =+ case WQO.merge w1 w2 of+ Just w' -> Sat w' `intersect` t2+ Nothing -> Unsat+intersect (Intersect t1 (Sat w1)) (Sat w2) =+ case WQO.merge w1 w2 of+ Just w' -> t1 `intersect` Sat w'+ Nothing -> Unsat+intersect (Intersect (Sat w1) t1) (Sat w2) =+ case WQO.merge w1 w2 of+ Just w' -> t1 `intersect` Sat w'+ Nothing -> Unsat+#endif+intersect t1 t2 = Intersect t1 t2++-- | @union c1 c2@ permits orderings of P1 and orderings of P2+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 o c@ strengthes @c@ to also contain every relation in @o@+addConstraint+ :: (Ord a, Hashable a) => WQO a -> ConstraintsADT a -> ConstraintsADT a+addConstraint o = intersect (Sat o)++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 = Implies (toSMT t2) (toSMT t1)++noConstraints :: ConstraintsADT a+noConstraints = Sat WQO.empty++unsatisfiable :: ConstraintsADT a+unsatisfiable = Unsat++{-# 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 = Mb.catMaybes+ (c1, c2) =+ if cost lhs > cost rhs+ then (lhs, rhs)+ else (rhs, lhs)++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 = toSMT++instance (Eq a, Hashable a, Show a) => Show (ConstraintsADT a) where+ 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)++-- | See 'ConstraintsADT'+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+ union+ unsatisfiable+ undefined+
+ src/Language/REST/WQOConstraints/Lazy.hs view
@@ -0,0 +1,120 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-}++-- | This module defines "Lazy" constraints on a WQO; the intention is that+-- computations on this type do only the necessary amount of work to determine+-- satisfiability (deferring further computations in a thunk).+module Language.REST.WQOConstraints.Lazy (+ lazyOC+ , addConstraint+ , isSatisfiable+ , noConstraints+ , LazyOC+ ) where++import Text.Printf+import GHC.Generics (Generic)+import Data.Hashable++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++-- | Implementation of "Lazy" ordering constraints.+data LazyOC a =+ Unsat+ -- @Sat wqo thunk@ represent satisfiable constraints; @wqo@ is a candidate.+ -- @Thunk@ represents the other satisfiable constraints, if any.+ | 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 lhs of+ Sat w t1' -> Sat w (ADT.union t1' rhs)+ Unsat -> eval rhs++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)++-- | Returns a new instance of 'LazyOC' permitting all WQOs+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)++-- | Returns @true@ if any orderings are permitted+isSatisfiable :: LazyOC a -> Bool+isSatisfiable (Sat _ _) = True+isSatisfiable Unsat = False++notStrongerThan :: (Monad m, Eq a) => LazyOC a -> LazyOC a -> m Bool+notStrongerThan _ Unsat = return True+notStrongerThan t1 t2 = return $ t1 == t2++-- | @addConstraint o c@ strengthes @c@ to also contain every relation in @o@+addConstraint :: (Ord a, Hashable a) => 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++-- | See 'LazyOC'+lazyOC :: Monad m => OC.WQOConstraints LazyOC m+lazyOC = OC.OC+ addConstraint+ intersect+ (return . isSatisfiable)+ notStrongerThan+ noConstraints+ permits+ union+ unsatisfiable+ getOrdering
+ src/Language/REST/WQOConstraints/Strict.hs view
@@ -0,0 +1,141 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ScopedTypeVariables #-}++-- | This module defines an implemenation for representing constraints on a 'WQO';+-- in this case represented by a set of "extendable" WQOs each satisfying the constraints.+-- For more details see 'StrictOC'+module Language.REST.WQOConstraints.Strict (+ strictOC+ , strictOC'+ , difference+ , isUnsatisfiable+ , noConstraints+ , permits+ , StrictOC+ ) 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)++-- | @StrictOC ws@ represents constraints on a WQO. Each element of @ws@ is a WQO+-- that satisfies the constraints. @StrictOC ws@ permits a WQO @w@ if there exists+-- a @w'@ in @ws@ such that @w'@ can be extended to yield @w@.+--+-- This implementation is similar to disjunctive normal form representation of+-- logical formulas; except in this case each "conjunction" is a valid WQO, and thus+-- "satisfiable". Therefore @StrictOC ws@ satisfies /some/ WQO iff @ws@ is not empty.+--+-- Two potential downsides to this implementation are:+-- 1. The size of @ws@ can grow quickly; an inherent issue of DNF+-- 2. Related, calculating the entire set @ws@ is computationally expensive,+-- and often unnecessary for RESTs use-case, where continuing the path only+-- requires knowing if /any/ WQO is permitted.+newtype 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))++getOrdering :: StrictOC a -> Maybe (WQO a)+getOrdering (StrictOC o) =+ listToMaybe (S.toList o)++-- | Constraints that permit any 'WQO'. In this case implemented by+-- a singleton set containing an empty WQO.+noConstraints :: forall a. (Eq a, Ord a, Hashable a) => StrictOC a+noConstraints = StrictOC (S.singleton WQO.empty)++unsatisfiable :: StrictOC a+unsatisfiable = StrictOC S.empty++-- | Returns @true@ iff @strictOC ws@ does not permit any WQOs; i.e., if @ws@ is 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'++-- | @StrictOC ws@ permits a 'WQO' @w@ if there exists a @w'@ in @ws@+-- that can be extended to equal @w@+permits :: (Eq a, Ord a, Hashable a) => StrictOC a -> WQO a -> Bool+permits (StrictOC permitted) desired =+ any (`WQO.notStrongerThan` desired) (S.toList permitted)++-- | An implementation of 'StrictOC'; for any computational context+strictOC :: Monad m => OC.WQOConstraints StrictOC m+strictOC = OC.OC+ addConstraint+ intersect+ (return . isSatisfiable)+ notStrongerThan+ noConstraints+ permits+ union+ unsatisfiable+ getOrdering++-- | An implementation of 'StrictOC' in the 'Identity' monad; usable in pure+-- computations.+strictOC' :: OC.WQOConstraints StrictOC Identity+strictOC' = strictOC
− src/Language/REST/WorkStrategy.hs
@@ -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"
− src/Lists.hs
@@ -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)- ]
− src/Main.hs
@@ -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 ()
− src/Multiset.hs
@@ -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))))"
− src/MultisetOrdering.hs
@@ -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)
− src/Nat.hs
@@ -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
− src/NonTerm.hs
@@ -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
− src/Set.hs
@@ -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₀))"
− src/WQODot.hs
@@ -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"
+ test/BagExample.hs view
@@ -0,0 +1,117 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveAnyClass #-}++{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+++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++newtype 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++newtype 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 _ _ = return S.empty+++fromPath :: [String] -> S.HashSet Rewrite+fromPath [] = S.empty+fromPath xs = S.fromList $ zipWith (curry go) 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+ , target = Nothing+ , workStrategy = bfs+ , ocImpl = impl+ , initRes = pathsResult+ , etStrategy = ExploreWhenNeeded+ } (bag start)+ let prettyPrinter = PrettyPrinter showRule showBag show ShowRejectsWithRule+ writeDot "example" Tree prettyPrinter (toOrderedSet paths)+ where+ impl = lift SC.strictOC $ cmapConstraints toMultiset (multisetOrder compareChar)
+ test/Compiler.hs view
@@ -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 [ ]
+ test/ExploredTerms.hs view
@@ -0,0 +1,45 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveAnyClass #-}++module ExploredTerms where++import Control.Monad.Identity+import Data.Hashable+import qualified Data.HashSet as S+import GHC.Generics (Generic)++import Language.REST.ExploredTerms as ET++type Constraints = Int++-- 2nd argument is cost to explore+data Term = Term String Int+ deriving (Eq, Generic, Hashable, Show)++exploreFuncs :: ExploreFuncs Term Constraints Identity+exploreFuncs = EF undefined subsume refine where+ subsume c0 c1 = return $ c0 >= c1+ refine c _ (Term _ dest) = c - dest++t0 :: Term+t0 = Term "t0" 5++t1 :: Term+t1 = Term "t1" 0++t2 :: Term+t2 = Term "t2" 0++et0 :: ExploredTerms Term Constraints Identity+et0 = ET.empty exploreFuncs ExploreWhenNeeded++et :: ExploredTerms Term Constraints Identity+et = ET.insert t1 15 (S.fromList [t0]) $ ET.insert t0 14 (S.fromList [t2]) et0++tests :: [(String, Bool)]+tests =+ [ -- Described in https://github.com/zgrannan/rest/issues/9+ ("Explore-opt", not $ runIdentity $ shouldExplore t1 17 et)++ , ("Explore", runIdentity $ shouldExplore t1 21 et)+ ]
+ test/Group.hs view
@@ -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)+ ]
+ test/KBO.hs view
@@ -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))")+ ]
+ test/LazyOC.hs view
@@ -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)+ )+ ]
+ test/Lists.hs view
@@ -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)+ ]
+ test/Main.hs view
@@ -0,0 +1,193 @@++{-# 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.Set as DS+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+import qualified Multiset as MS+import NonTerm as NT+import qualified Lists as Li++import Language.REST.Core+import Language.REST.ConcreteOC+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 :: ShowRejectsOpt+ , gUseETOpt :: Bool+ }++defaultParams :: GraphParams+defaultParams = GraphParams False Nothing Tree ShowRejectsWithoutRule 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 = HideRejects}++withShowRejectsRule :: GraphParams -> GraphParams+withShowRejectsRule gp = gp{gShowRejects = ShowRejectsWithRule}++data SolverType = LPOStrict | LPO | RPO | RPOConcrete [Op] | 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 (RPOConcrete ops) evalRWs0 userRWs0 name term0 params =+ mkRESTGraph' (concreteOC $ DS.fromList ops) 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_ (putStrLn . pr) $ S.toList userRWs0+ liftIO $ mapM_ (putStrLn . pr) $ S.toList evalRWs0+ start <- liftIO getCurrentTime+ (PathsResult paths, targetPath) <- rest+ RESTParams+ { re = evalRWs0+ , ru = userRWs0+ , 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 ()++setDistribRules :: S.HashSet Rewrite+setDistribRules = S.fromList+ [ distribL (/\) (\/)+ , distribR (/\) (\/)+ , distribL (\/) (/\)+ , distribR (\/) (/\)+ ]++challengeRulesNoCommute :: S.HashSet Rewrite+challengeRulesNoCommute = S.union setDistribRules $ S.fromList+ [ x /\ x ~> x+ , x \/ x ~> x+ , x \/ emptyset ~> x+ , x /\ emptyset ~> emptyset+ , 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
+ test/Multiset.hs view
@@ -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))))"
test/MultisetOrder.hs view
@@ -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)@@ -29,7 +31,7 @@ tests :: [(String, Bool)] tests = [ ("Constraints",- (SC.noConstraints /=- (runIdentity $ ms SC.noConstraints (M.fromList "bc") (M.fromList "aa"))))+ SC.noConstraints /=+ runIdentity (ms SC.noConstraints (M.fromList "bc") (M.fromList "aa"))) , ("Unsat", SC.isUnsatisfiable $ runIdentity unsat) ]
+ test/NonTerm.hs view
@@ -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
test/OpOrdering.hs view
@@ -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 (@@ -22,11 +22,11 @@ ) ] where - Just wqo = mergeAll [ ("cons" =. "z")- , ("g" =. "nil")- , ("h" =. "s")- , ("cons" >. "g")- , ("cons" >. "h")- , ("h" >. "f")- , ("h" >. "g")+ Just wqo = mergeAll [ "cons" =. "z"+ , "g" =. "nil"+ , "h" =. "s"+ , "cons" >. "g"+ , "cons" >. "h"+ , "h" >. "f"+ , "h" >. "g" ]
test/QuickCheckTests.hs view
@@ -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)@@ -56,7 +54,7 @@ let po' = fromMaybe po $ PO.insert po f g go po' (n - 1) -gen_wqo_steps :: Gen ([(Op, Op, WQO.QORelation)])+gen_wqo_steps :: Gen [(Op, Op, WQO.QORelation)] gen_wqo_steps = do numOps <- choose (0, 10)@@ -85,7 +83,7 @@ where go :: Int -> Gen RuntimeTerm go sz = do- (op, arity) <- oneof $ map return $ (filter ((<= sz) . snd) syms)+ (op, arity) <- oneof $ map return $ filter ((<= sz) . snd) syms args <- vectorOf arity (go (sz `div` (arity + 1))) return $ App (Op op) args @@ -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,7 +133,8 @@ constraints = rpoGTE t u ordering = Mb.fromJust (OC.getOrdering impl constraints) -prop_permits steps = SC.permits (SC.noConstraints) (toWQO steps)+prop_permits :: [(Op, Op, WQO.QORelation)] -> Bool+prop_permits steps = SC.permits SC.noConstraints (toWQO steps) -- Should fail -- If this prop was true, we'd only ever need to check each term once@@ -138,6 +148,7 @@ -- where -- types = t0::RuntimeTerm +tests :: IO [()] tests = sequence [ -- quickCheckWith stdArgs{maxDiscardRatio = 1000} prop_rpot2
test/RPO.hs view
@@ -3,54 +3,63 @@ 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 xs = go (OC.noConstraints ?impl) xs where- go c (t:u:xs) = OC.intersect ?impl c (rpoGTE t u)+rpoSeq+ :: (?impl::WQOConstraints impl m, Show (impl Op), Eq (impl Op), Hashable (impl Op))+ => [RuntimeTerm]+ -> impl Op+rpoSeq = go (OC.noConstraints ?impl) where+ 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" g = Op "g" h = Op "h" in- [ ("RPO1", return $ (rpoGTE "f(z)" "g(s(z))")+ [ ("RPO1", return $ rpoGTE "f(z)" "g(s(z))" == OC.intersect ?impl (OC.singleton ?impl (f >. g)) (OC.singleton ?impl (f >. s))) , ("RPO2", isUnsatisfiable ?impl $ OC.intersect ?impl@@ -64,8 +73,8 @@ , ("SynGTE", return $ synGTE OpOrdering.empty (App s [App s [App g [App (Op "+") [App h [App s [App z []]],App z []],App s [App s [App g [App z [],App z []]]]]]]) (App z [])) , ("SynGTE2", return $ synGTE (Mb.fromJust $ mergeAll [- ("cons" >. g)- , (f >. s)- , (h >. g)- , (h >. "nil")]) "s(cons(h(h(z)), f(nil, nil, z)))" "g(z, cons(g(nil, nil), s(s(z))))")+ "cons" >. g+ , f >. s+ , h >. g+ , h >. "nil"]) "s(cons(h(h(z)), f(nil, nil, z)))" "g(z, cons(g(nil, nil), s(s(z))))") ]
+ test/SMT.hs view
@@ -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)]
test/StrictOC.hs view
@@ -3,22 +3,21 @@ 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) , ("permits2", permits noConstraints $ fromJust $ parseOO "+ = f = nil = s ∧ + > g ∧ + > h ∧ cons > + ∧ cons > g") ] where- Just wqo = mergeAll [ ("cons" =. "z")- , ("g" =. "nil")- , ("h" =. "s")- , ("cons" >. "g")- , ("cons" >. "h")- , ("h" >. "f")- , ("h" >. "g")+ Just wqo = mergeAll [ "cons" =. "z"+ , "g" =. "nil"+ , "h" =. "s"+ , "cons" >. "g"+ , "cons" >. "h"+ , "h" >. "f"+ , "h" >. "g" ]
test/Test.hs view
@@ -1,62 +1,83 @@ {-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RankNTypes #-} module Main where +import qualified Data.List as L import Data.Hashable+#if MIN_VERSION_mtl(2,3,0)+import Control.Monad (guard)+#endif import Control.Monad.Identity import qualified Arith as A+ import qualified Data.HashMap.Strict as M+import qualified ExploredTerms import OpOrdering import DSL-import WQO as WQO-import MultisetOrder as MultisetOrder+import WQO+import MultisetOrder import Nat-import RPO as RPO-import StrictOC as StrictOC-import LazyOC as LazyOC-import qualified QuickCheckTests as QuickCheckTests+import RPO+import KBO+import StrictOC+import LazyOC+import SMT+import qualified 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.RewriteRule import Language.REST.RuntimeTerm import Language.REST.MetaTerm as MT-import Language.REST.Rewrite+import Language.REST.Internal.Rewrite+import Language.REST.Internal.WQO 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) +-- | 'canOrient' returns true iff the ordering constraint algebra permits an ordering+-- that orients, the path, i.e., the constraints generated by 'orient' are satisfiable.+canOrient :: forall oc m . Show oc+ => (?impl :: OCAlgebra oc RuntimeTerm m) => [RuntimeTerm] -> m Bool+canOrient terms = isSat ?impl (orient ?impl terms)++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 =- terms <$> fst <$> rest+ => OCAlgebra oc RuntimeTerm IO+ -> S.HashSet Rewrite -> S.HashSet Rewrite -> RuntimeTerm -> IO (S.HashSet RuntimeTerm)+rewrites impl evalRWs userRWs t0 =+ resultTerms . fst <$> rest RESTParams { re = evalRWs , ru = userRWs- , toET = id , target = Nothing , workStrategy = notVisitedFirst , ocImpl = ?impl , initRes = termsResult+ , etStrategy = ExploreWhenNeeded } t0+ where+ ?impl = impl runTest :: (String, IO Bool) -> IO () runTest (name, test) = do@@ -77,52 +98,59 @@ 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))- , ("simple2", return $ (rpoGTE "f(t1)" "g(t2)") `permits'` (Mb.fromJust $ merge (f >. g) (t1Op =. t2Op)))- , ("simple3", return $ (rpoGTE "f(t1)" "g(t2)") `permits'` (Mb.fromJust $ merge (f >. g) (t1Op >. t2Op)))+ ("simple1", return $ not $ rpoGTE "f(t1)" "g(t2)" `permits'` (t1Op =. t2Op))+ , ("simple2", return $ rpoGTE "f(t1)" "g(t2)" `permits'` Mb.fromJust (merge (f >. g) (t1Op =. t2Op)))+ , ("simple3", return $ rpoGTE "f(t1)" "g(t2)" `permits'` Mb.fromJust (merge (f >. g) (t1Op >. t2Op))) , ("subterm", return $ rpoGTE "f(g)" "f" == noConstraints ?impl) , ("intersect", OC.isUnsatisfiable ?impl $ OC.intersect ?impl (OC.singleton ?impl (f >. g)) (OC.singleton ?impl (g >. f))) ] 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 =+eval :: S.HashSet Rewrite -> RuntimeTerm -> IO RuntimeTerm+eval rws t0 =+ do+ result <- mapM (apply t0) (S.toList rws)+ case S.toList $ S.unions result of+ [] -> return t0+ (t : _) -> eval rws t++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- , (intToTerm 1) .+ t1- ]- ))- , ("Diverge3", not <$> (diverges [ (t1 .+ t2) .+ t3+ , ("Diverge", not <$> diverges impl [ intToTerm 2 .+ t1+ , intToTerm 1 .+ t1+ ])+ , ("Diverge3", not <$> diverges impl [ (t1 .+ t2) .+ t3 , t1 .+ (t2 .+ t3) , (t2 .+ t3) .+ t1- ]- ))+ ]) , ("Eval1", arithEQ (intToTerm 2 .+ intToTerm 3) 5) , ("Eval2", arithEQ (ack (intToTerm 3) (intToTerm 2)) 29)- , ("Subst1", return $ subst (M.fromList [("x", intToTerm 1), ("y", intToTerm 2)]) (x #+ y) == (intToTerm 1 .+ intToTerm 2))+ , ("Subst1", return $ subst (M.fromList [("X", intToTerm 1), ("Y", intToTerm 2)]) (x #+ y) == (intToTerm 1 .+ intToTerm 2)) , ("ArithTerm", termTest) , ("ArithTerm2", termTest2) , ("Arith0", eq (t1 .+ t2 .+ intToTerm 1) (t1 .+ (intToTerm 1 .+ t2)))@@ -144,38 +172,38 @@ 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 []]) )+ , ("EvalComplete2" , (== App finish []) <$> eval completeUserRWs (App start' [App s1 []]) ) , ("Complete2" , eq (App start' [App s1 []]) (App finish [])) ] where@@ -190,7 +218,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 +230,7 @@ s1 = Op "s1" s2 = Op "s2" +ocTests :: (Handle, Handle) -> IO () ocTests z3 = do runTestSuite "LazyOC" LazyOC.tests runTestSuite "StrictOC" StrictOC.tests@@ -212,16 +241,30 @@ 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 "ExploredTerms" ExploredTerms.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
test/WQO.hs view
@@ -1,6 +1,7 @@ module WQO where -import Language.REST.WQO as WQO+import Language.REST.Internal.WQO as WQO+import Data.Maybe (isNothing) basicInvalid :: Maybe (WQO Char) basicInvalid = do@@ -14,5 +15,5 @@ ValidExtension fgyz = insert fg ("y", "z", QGT) in [ ("NotStrongerThan", fg `notStrongerThan` fgyz)- , ("RejectInvalid", basicInvalid == Nothing)+ , ("RejectInvalid", isNothing basicInvalid) ]
+ test/WQODot.hs view
@@ -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"
+ testlib/Arith.hs view
@@ -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]
+ testlib/DSL.hs view
@@ -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 ]
+ testlib/Language/REST/ConcreteOC.hs view
@@ -0,0 +1,32 @@+{-# 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.Op++import Data.Hashable+import GHC.Generics (Generic)+import qualified Data.Set as S++newtype ConcreteOC = ConcreteOC (S.Set (WQO.WQO Op))+ deriving (Eq, Ord, Generic, Hashable)++instance Show ConcreteOC where+ show (ConcreteOC ords) = show (S.size ords) ++ " orderings"++concreteOC :: Monad m => S.Set Op -> AOC.OCAlgebra ConcreteOC RuntimeTerm m+concreteOC ops = AOC.OCAlgebra (return . isSat) refine (ConcreteOC (WQO.orderings ops)) union notStrongerThan+ where+ union (ConcreteOC ord1) (ConcreteOC ord2) = ConcreteOC $ S.union ord1 ord2+ notStrongerThan (ConcreteOC ord1) (ConcreteOC ord2) = return $ ord1 == ord2 || ord2 `S.isSubsetOf` ord1++ isSat :: ConcreteOC -> Bool+ isSat (ConcreteOC ords) = not $ S.null ords++ refine :: ConcreteOC -> RuntimeTerm -> RuntimeTerm -> ConcreteOC+ refine (ConcreteOC ords) t u = ConcreteOC (S.filter (\ord -> synGTE ord t u) ords)
+ testlib/Language/REST/ProofGen.hs view
@@ -0,0 +1,54 @@+{-# 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) (unwords $ 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 = zipWith (curry proofStep) 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 = maybe "lemma" T.pack name++ 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
+ testlib/MultisetOrdering.hs view
@@ -0,0 +1,143 @@+{-# 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)++newtype 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 =+ let+ (lts, us') = L.partition (t `gt`) us+ in+ go (Replace t lts : rs) ts us'+ go rs ts [] = Just $ MultisetGE $ map (`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 $ Mb.mapMaybe 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 = Mb.fromMaybe (tindex, tsIndex) (Mp.lookup (tindex, tsIndex) mp)++ 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)
+ testlib/Nat.hs view
@@ -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 = pack . Prelude.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 (Prelude.show err)+ Right t -> t++instance IsString RuntimeTerm where+ fromString = parseTerm
+ testlib/Set.hs view
@@ -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₀))"