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