rest-rewrite (empty) → 0.1
raw patch · 50 files changed
+4252/−0 lines, 50 filesdep +QuickCheckdep +basedep +containers
Dependencies added: QuickCheck, base, containers, hashable, monad-loops, mtl, parsec, process, text, time, unordered-containers
Files
- LICENSE +11/−0
- rest-rewrite.cabal +165/−0
- src/Arith.hs +41/−0
- src/BagExample.hs +114/−0
- src/Compiler.hs +29/−0
- src/DSL.hs +77/−0
- src/Group.hs +23/−0
- src/Language/REST.hs +49/−0
- src/Language/REST/AbstractOC.hs +32/−0
- src/Language/REST/ConcreteOC.hs +57/−0
- src/Language/REST/Core.hs +63/−0
- src/Language/REST/Dot.hs +77/−0
- src/Language/REST/EquivalenceClass.hs +73/−0
- src/Language/REST/ExploredTerms.hs +93/−0
- src/Language/REST/MetaTerm.hs +34/−0
- src/Language/REST/MultiSet.hs +80/−0
- src/Language/REST/MultisetOrder.hs +79/−0
- src/Language/REST/OCToAbstract.hs +53/−0
- src/Language/REST/Op.hs +41/−0
- src/Language/REST/OpOrdering.hs +104/−0
- src/Language/REST/OrderingConstraints.hs +113/−0
- src/Language/REST/OrderingConstraints/ADT.hs +244/−0
- src/Language/REST/OrderingConstraints/Lazy.hs +118/−0
- src/Language/REST/OrderingConstraints/Strict.hs +152/−0
- src/Language/REST/PartialOrder.hs +98/−0
- src/Language/REST/Path.hs +33/−0
- src/Language/REST/RESTDot.hs +100/−0
- src/Language/REST/RPO.hs +175/−0
- src/Language/REST/Rest.hs +188/−0
- src/Language/REST/Rewrite.hs +56/−0
- src/Language/REST/RewriteRule.hs +8/−0
- src/Language/REST/RuntimeTerm.hs +39/−0
- src/Language/REST/SMT.hs +109/−0
- src/Language/REST/Types.hs +79/−0
- src/Language/REST/WQO.hs +329/−0
- src/Language/REST/WorkStrategy.hs +37/−0
- src/Lists.hs +34/−0
- src/Main.hs +151/−0
- src/Multiset.hs +44/−0
- src/MultisetOrdering.hs +141/−0
- src/Nat.hs +99/−0
- src/NonTerm.hs +29/−0
- src/WQODot.hs +21/−0
- test/MultisetOrder.hs +35/−0
- test/OpOrdering.hs +32/−0
- test/QuickCheckTests.hs +153/−0
- test/RPO.hs +71/−0
- test/StrictOC.hs +24/−0
- test/Test.hs +227/−0
- test/WQO.hs +18/−0
+ LICENSE view
@@ -0,0 +1,11 @@+Copyright 2021 Zack Grannan++Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:++1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.++3. Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ rest-rewrite.cabal view
@@ -0,0 +1,165 @@+name: rest-rewrite+build-type: Simple+version: 0.1+cabal-version: 1.22+category: Rewriting+maintainer: Zack Grannan <zgrannan@cs.ubc.ca>+license: BSD3+description: Rewriting library with online termination checking.+synopsis: Rewriting library with online termination checking+license-file: LICENSE++library+ default-language: Haskell2010+ exposed-modules:+ Language.REST+ Language.REST.AbstractOC+ Language.REST.Core+ Language.REST.ExploredTerms+ Language.REST.MetaTerm+ Language.REST.Dot+ Language.REST.RESTDot+ Language.REST.Op+ Language.REST.OrderingConstraints+ Language.REST.OrderingConstraints.Strict+ Language.REST.OrderingConstraints.Lazy+ Language.REST.OrderingConstraints.ADT+ Language.REST.Path+ 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++ hs-source-dirs: src+ build-depends: base >= 4.7 && < 5+ , containers >= 0.6.2 && < 0.7+ , hashable >= 1.3.0 && < 1.4+ , process >= 1.6.9 && < 1.7+ , parsec >= 3.1.14 && < 3.2+ , mtl >= 2.2.2 && < 2.3+ , unordered-containers >= 0.2.13 && < 0.3+ , text >= 1.2.4 && < 1.3++Test-Suite test-rest+ default-language: Haskell2010+ type: exitcode-stdio-1.0+ main-is: Test.hs+ hs-source-dirs: test src+ build-depends: base+ , hashable+ , containers+ , parsec+ , QuickCheck >= 2.14.2 && < 2.15+ , mtl+ , unordered-containers+ , text+ , process+ 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+ MultisetOrder+ Nat+ OpOrdering+ QuickCheckTests+ RPO+ StrictOC+ WQO++++executable rest+ default-language: Haskell2010+ main-is: Main.hs+ -- ghc-plugins: -fplugin=LiquidHaskell+ build-depends: base >= 4.7+ , containers+ , hashable+ , process+ , QuickCheck+ , parsec+ , mtl+ , monad-loops >= 0.4.3 && < 0.5+ , unordered-containers >= 0.2.11+ , text >= 1.2.2+ , time >= 1.9.3 && < 1.10+ -- , liquidhaskell+ -- , liquid-base+ other-modules:+ Arith+ BagExample+ DSL+ Group+ Language.REST.AbstractOC+ Language.REST.ConcreteOC+ Language.REST.Core+ 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.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+ Compiler+ Lists+ Multiset+ MultisetOrdering+ Nat+ NonTerm+ WQODot+ Language.REST.Dot+ Language.REST.RESTDot++ hs-source-dirs: src
+ src/Arith.hs view
@@ -0,0 +1,41 @@+{-# 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 view
@@ -0,0 +1,114 @@+{-# 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 view
@@ -0,0 +1,29 @@+{-# 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 view
@@ -0,0 +1,77 @@+{-# 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 view
@@ -0,0 +1,23 @@+{-# 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
@@ -0,0 +1,49 @@+-- |++module Language.REST where++import Control.Monad.Identity+import Data.Hashable+import Data.Maybe+import qualified Data.HashSet as S+import qualified Data.HashMap.Strict as M++import Language.REST.Types+import Language.REST.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.RPO+import Language.REST.RuntimeTerm+import Language.REST.Op+import Language.REST.OpOrdering+import qualified Language.REST.WQO as WQO+++adtRPO z3 = lift (adtOC z3) rpo+-- lazyRPO = lift lazyOC rpo+-- strictRPO = lift strictOC rpo++-- Assume vars are arity 0, which is usually correct+getVars :: RuntimeTerm -> S.HashSet Op+getVars (App op []) = S.singleton op+getVars (App op xs) = S.unions (map getVars xs)+++varsEQ :: RuntimeTerm -> RuntimeTerm -> WQO.WQO Op+varsEQ t1 t2 =+ let+ vars = getVars t1 `S.union` getVars t2+ in+ fromJust $ WQO.mergeAll (map (uncurry (=.)) (pairs (S.toList vars)))+ where+ pairs xs | length xs < 2 = []+ pairs xs | otherwise = zip xs (tail xs)++cgen :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RuntimeTerm Identity+cgen impl r oc t1 t2 =+ let+ Identity rpoc = rpo impl r oc t1 t2+ in+ return $ addConstraint impl (varsEQ t1 t2) rpoc
+ src/Language/REST/AbstractOC.hs view
@@ -0,0 +1,32 @@+{-# 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 view
@@ -0,0 +1,57 @@+{-# 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
@@ -0,0 +1,63 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ImplicitParams #-}++module Language.REST.Core where++import Prelude hiding (GT, EQ)++import Debug.Trace ( trace )+import Data.Functor.Identity+import qualified Data.List as L+import qualified Data.HashSet as S++import Language.REST.AbstractOC+import Language.REST.Op+import Language.REST.OrderingConstraints+import Language.REST.RPO+import Language.REST.OpOrdering as OO+import Language.REST.Types+import qualified Language.REST.MetaTerm as MT+import Language.REST.WQO+import Language.REST.Rewrite+import Language.REST.RuntimeTerm as RT+import Language.REST.RewriteRule++type MetaTerm = MT.MetaTerm+++contains :: RuntimeTerm -> RuntimeTerm -> Bool+contains t1 t2 | t1 == t2 = True+contains (App _ ts) t = any (contains t) ts+++orient' :: Show oc => (?impl :: AbstractOC 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)++canOrient :: forall oc m . Show oc+ => (?impl :: AbstractOC oc RuntimeTerm m) => [RuntimeTerm] -> m Bool+canOrient terms = trace ("Try to orient " ++ termPathStr terms) $ isSat ?impl (orient terms)++syms :: MetaTerm -> S.HashSet String+syms (MT.Var s) = S.singleton s+syms (MT.RWApp _ xs) = S.unions (map syms xs)++termPathStr :: [RuntimeTerm] -> String+termPathStr terms = L.intercalate " --> \n" (map pp terms)+ where+ pp = prettyPrint (PPArgs [] [] (const Nothing))++eval :: S.HashSet Rewrite -> RuntimeTerm -> IO RuntimeTerm+eval rws t =+ do+ result <- mapM (apply t) (S.toList rws)+ case S.toList $ S.unions result of+ [] -> return t+ (t : _) -> eval rws t
+ src/Language/REST/Dot.hs view
@@ -0,0 +1,77 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Language.REST.Dot where++import GHC.Generics+import Data.Hashable+import Data.List+import qualified Data.Set as S+import Text.Printf+import System.Process++data DiGraph = DiGraph String (S.Set Node) (S.Set Edge);++type NodeID = String++data GraphType = Tree | Dag | Min deriving (Read)++data Node = Node + { nodeID :: NodeID+ , label :: String+ , nodeStyle :: String+ , labelColor :: String+ } deriving (Eq, Ord, Show, Generic, Hashable)++data Edge = Edge+ { from :: NodeID+ , to :: NodeID+ , edgeLabel :: String+ , edgeColor :: String+ , subLabel :: String+ , edgeStyle :: String+ } deriving (Eq, Ord, Show, Generic, Hashable)++type DotPath = [Node]++nodeString :: Node -> String+nodeString (Node id label style color) = + printf "\t%s [label=\"%s\"\nstyle=\"%s\"\ncolor=\"%s\"];" id label style color++edgeString :: Edge -> String+edgeString (Edge from to label color subLabel style) = + let + sub = escape subLabel+ escape xs = concatMap go xs+ where+ go '\\' = "\\"+ go '\n' = "<br />"+ go '>' = ">"+ go o = [o]+ labelPart =+ if label /= ""+ then printf "<font color =\"red\">%s</font>" label+ else ""+ in+ printf "\t%s -> %s [label = <%s<br/>%s>\ncolor=\"%s\"\nstyle=\"%s\"];" from to labelPart sub color style++graphString :: DiGraph -> String+graphString (DiGraph name nodes edges) = + printf "digraph %s {\n%s\n\n%s\n}" name (nodesString) (edgesString)+ where+ nodesString :: String+ nodesString = intercalate "\n" (map nodeString (S.toList nodes))++ edgesString :: String+ edgesString = intercalate "\n" (map edgeString (S.toList edges))+++mkGraph :: String -> DiGraph -> IO ()+mkGraph name graph = do+ let dotfile = printf "graphs/%s.dot" name+ let pngfile = printf "graphs/%s.png" name+ writeFile dotfile (graphString graph)+ result <- readProcessWithExitCode "dot" ["-Tpng", dotfile, "-o", pngfile] ""+ print result+
+ src/Language/REST/EquivalenceClass.hs view
@@ -0,0 +1,73 @@+{-# 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
@@ -0,0 +1,93 @@+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE ScopedTypeVariables #-}+module Language.REST.ExploredTerms+ (+ ExploredTerms+ , empty+ , insert+ , shouldExplore+ , size+ , visited+ , ExploreFuncs(..)+ ) where++import Debug.Trace+import qualified Data.HashMap.Strict as M+import qualified Data.HashSet as S+import Data.Hashable++import Prelude hiding (lookup)++data ExploreStrategy =+ ExploreAlways | ExploreLessConstrained | ExploreWhenNeeded | ExploreOnce++data ExploreFuncs c m = EF+ { union :: c -> c -> c+ , subsumes :: c -> c -> m Bool+ }++-- A mapping of terms, to the rewritten terms that need to be fully explored+-- in order for this term to be fully explored+data ExploredTerms term c m =+ ET (M.HashMap term (c, (S.HashSet term))) (ExploreFuncs c m) ExploreStrategy++-- trace' = trace+trace' _ x = x+++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++visited :: (Eq term, Hashable term) => term -> ExploredTerms term c m -> Bool+visited t (ET m _ _) = M.member t m++insert :: (Eq term, Hashable term) => term -> c -> S.HashSet term -> ExploredTerms term c m -> ExploredTerms term c m+insert t oc s (ET etMap ef@(EF union _ ) strategy) = ET (M.insertWith go t (oc, s) etMap) ef strategy+ where+ go (oc1, s1) (oc2, s2) = (union oc1 oc2, S.union s1 s2)++lookup :: (Eq term, Hashable term) => term -> ExploredTerms term c m -> Maybe (c, (S.HashSet term))+lookup t (ET etMap _ _) = M.lookup t etMap++isFullyExplored :: forall term c m . (Monad m, Show term, Eq term, Hashable term, Eq c) =>+ term -> c -> ExploredTerms term c m -> m Bool+isFullyExplored t0 oc0 et@(ET _ (EF{subsumes}) _) = result where++ result = go S.empty [t0]+ -- if (trace ("Check " ++ show t0) go) S.empty [t0]+ -- then trace (show t0 ++ " is fully explored.") True+ -- else False++ go :: S.HashSet term -> [term] -> m Bool+ go _ [] = return True+ go seen (h:t) | Just (oc, trms) <- lookup h et+ = do+ ns <- oc `subsumes` oc0+ if ns+ then go seen' t+ else+ let ts = (S.union trms (S.fromList t)) `S.difference` seen'+ in go seen' (S.toList ts)+ where+ seen' = S.insert h seen++ go _ _ | otherwise = trace' "GF" $ return False -- trace ("Must check " ++ show t0 ++ " . Visited: " ++ (show $ visited t0 et)) False++shouldExplore :: forall term c m . (Monad m, Show term, Eq term, Hashable term, Eq c, Show c) =>+ term -> c -> ExploredTerms term c m -> m Bool+shouldExplore t oc et@(ET _ EF{subsumes} strategy) =+ case strategy of+ ExploreWhenNeeded -> not <$> isFullyExplored t oc et+ ExploreOnce -> return $ not $ visited t et+ ExploreAlways -> return True+ ExploreLessConstrained ->+ case lookup t et of+ Just (oc', _) -> do+ s <- oc' `subsumes` oc+ return $ if s+ then trace' ((show oc') ++ " subsumes " ++ (show oc)) False+ else True+ Nothing -> return True
+ src/Language/REST/MetaTerm.hs view
@@ -0,0 +1,34 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}++module Language.REST.MetaTerm where++import Data.String+import Data.Hashable+import GHC.Generics (Generic)+import qualified Data.Set as S++import Language.REST.Op+import Language.REST.RuntimeTerm++data MetaTerm =+ Var String+ | RWApp Op [MetaTerm] deriving (Eq, Ord, Show, Generic, Hashable)++instance IsString MetaTerm where+ fromString = Var++class ToMetaTerm a where+ toMetaTerm :: a -> MetaTerm++instance ToMetaTerm MetaTerm where+ toMetaTerm = id++instance ToMetaTerm RuntimeTerm where+ toMetaTerm (App f xs) = RWApp f (map toMetaTerm xs)++termOps :: ToMetaTerm a => a -> S.Set Op+termOps = go . toMetaTerm where+ go :: MetaTerm -> S.Set Op+ go (Var _) = S.empty+ go (RWApp op trms) = S.insert op (S.unions (map go trms))
+ src/Language/REST/MultiSet.hs view
@@ -0,0 +1,80 @@+{-# 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 view
@@ -0,0 +1,79 @@+{-# 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/OCToAbstract.hs view
@@ -0,0 +1,53 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}++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.Types+import Language.REST.SMT++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.ConstraintGen impl base lifted Identity+ -> AbstractOC (impl base) lifted m+lift oc cgen =+ AbstractOC {+ isSat = isSat'+ , top = top'+ , refine = refine'+ , union = OC.union oc+ , notStrongerThan = OC.notStrongerThan oc+ }+ where+ isSat' :: impl base -> m Bool+ isSat' aoc = OC.isSatisfiable oc aoc++ top' :: impl base+ top' = OC.noConstraints oc++ 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+ in+ result++-- trace' _ x = x+trace' = trace
+ src/Language/REST/Op.hs view
@@ -0,0 +1,41 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE OverloadedStrings #-}++module Language.REST.Op where++import Data.Text as T+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)++instance Show Op where+ show (Op o) = unpack o++instance IsString Op where+ fromString = Op . pack++instance ToSMTVar Op Int where+ toSMTVar (Op "ite") = SMTVar "_ite_"+ toSMTVar (Op op) = SMTVar $ T.append "op_" $ T.concatMap go op+ where+ go '∅' = "_empty_"+ go '₀' = "0"+ go '₁' = "1"+ go '$' = "_dollar_"+ go '[' = "_lb_"+ go ']' = "_rb_"+ go ':' = "_colon_"+ go '.' = "_dot_"+ go '#' = "_pound_"+ go '\'' = "_comma_"+ go '/' = "_slash_"+ go ' ' = "_space_"+ go '∪' = "_cup_"+ go '\\' = "_bslash_"+ go c = singleton c
+ src/Language/REST/OpOrdering.hs view
@@ -0,0 +1,104 @@+{-# 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 view
@@ -0,0 +1,113 @@+{-# 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 view
@@ -0,0 +1,244 @@+{-# 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 view
@@ -0,0 +1,118 @@+{-# 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 view
@@ -0,0 +1,152 @@+{-# 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 view
@@ -0,0 +1,98 @@+{-# 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
@@ -0,0 +1,33 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE FlexibleInstances #-}++module Language.REST.Path where++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+ , rule :: rule+ , ordering :: a+ , fromPLE :: Bool+} deriving (Eq, Ord, Generic, Hashable)+++data PathTerm rule term = PathTerm+ { pathTerm :: term++ -- The orderings FROM pathTerm that were rejected+ , rejected :: S.HashSet (term, rule)+ } deriving (Eq, Ord, Generic, Hashable)++type Path rule term a = ([Step rule term a], PathTerm rule term)++pathTerms :: Path rule term a -> [term]+pathTerms (xs, x) = map pathTerm $ map term xs ++ [x]++runtimeTerm :: Path rule term a -> term+runtimeTerm (_, pt) = pathTerm pt
+ src/Language/REST/RESTDot.hs view
@@ -0,0 +1,100 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+module Language.REST.RESTDot where++import Data.List+import Data.Hashable+import qualified Data.Set as S+import qualified Data.HashSet as HS++import Language.REST.Dot+import Language.REST.Path+import Language.REST.Types++data PrettyPrinter rule term ord = PrettyPrinter+ { printRule :: rule -> String+ , printTerm :: term -> String+ , printOrd :: ord -> String+ , showRejects :: Bool+ }++rejNodeID :: (Hashable rule, Hashable term, Hashable a) => GraphType -> Path rule term a -> term -> String+rejNodeID gt p term = getNodeID gt p ++ show (abs $ hash term)++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)+ where+ go :: (term, rule) -> Node+ go (term, r) = Node (rejNodeID gt p term) (printTerm pp term) "dashed" "red"+++getNodeID :: (Hashable rule, Hashable term, Hashable a) => GraphType -> Path rule term a -> String+getNodeID Tree p = "node" ++ show (abs $ hash p)+getNodeID Dag (steps, t) =+ "node" ++ show (abs $ hash t) ++ "_" ++ show (length steps)+getNodeID Min (_, t) = "node" ++ show (abs $ hash t)++-- This determines how to layout+endNode :: (Hashable rule, Hashable term, Hashable a)+ => GraphType -> PrettyPrinter rule term a -> Path rule term a -> Node+endNode gt pp p@(_, t) =+ let+ nodeID = getNodeID gt p+ in+ Node nodeID (printTerm pp (pathTerm t)) "solid" "black"++toEdges :: forall rule term a . (Hashable rule, Hashable term, Hashable a) =>+ GraphType -> PrettyPrinter rule term a -> Path rule term a -> S.Set Edge+toEdges gt pp path = allRej `S.union` (S.fromList $ map toEdge (zip subs (tail subs)))+ where+ subs = subPaths path++ allRej = S.unions $ map rejEdges subs++ rejEdges :: Path rule term a -> S.Set Edge+ rejEdges p@(_, PathTerm _ rej) =+ if showRejects pp+ 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"+++ toEdge :: (Path rule term a, Path rule term a) -> Edge+ toEdge (p0, p1@(ts, _)) =+ let+ step = last ts+ color = if (fromPLE step) then "brown" else "darkgreen"+ subLabel = printOrd pp (ordering step)+ startNodeID = nodeID (endNode gt pp p0)+ endNodeID = nodeID (endNode gt pp p1)+ in+ Edge startNodeID endNodeID (printRule pp (rule step)) color subLabel "solid"++subPaths :: Path rule term a -> [Path rule term a]+subPaths p@(xs, t) = map toPath (tail $ inits xs) ++ [p]+ where+ toPath xs = (init xs, term (last xs))++toNodes :: (Hashable rule, Hashable term, Hashable a) => GraphType -> PrettyPrinter rule term a -> Path rule term a -> S.Set Node+toNodes gt pp path =+ let+ r = S.unions $ map (rejectedNodes gt pp) (subPaths path)+ n = S.fromList (map (endNode gt pp) (subPaths path))+ in+ S.union r n++toGraph :: (Hashable rule, Hashable term, Hashable a) => GraphType -> PrettyPrinter rule term a -> S.Set (Path rule term a) -> DiGraph+toGraph gt pp paths =+ DiGraph "Rest" (unions (S.map (toNodes gt pp) paths)) (unions (S.map (toEdges gt pp) paths))+ where+ unions :: (Ord a, Eq a, Hashable a) => S.Set (S.Set a) -> S.Set a+ unions = S.unions . S.toList++writeDot :: (Hashable rule, Hashable term, Ord a, Hashable a) =>+ String -> GraphType -> PrettyPrinter rule term a -> S.Set (Path rule term a) -> IO ()+writeDot name gt printer paths = mkGraph name (toGraph gt printer paths)+
+ src/Language/REST/RPO.hs view
@@ -0,0 +1,175 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ImplicitParams #-}++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 Language.REST.Op+import Language.REST.OpOrdering as OpOrdering+import Language.REST.OrderingConstraints 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)++instance Show RuntimeTerm where+ show (App op trms) =+ if MS.null trms+ then show op+ else show op ++ show trms++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))++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)++data RPOState oc =+ RPOState+ { rpoCache :: Cache oc+ , rpoDepth :: Int+ }++type RMonad oc = State (RPOState oc)++incDepth :: RMonad oc (oc Op) -> RMonad oc (oc Op)+incDepth action = do+ modify (\st -> st{rpoDepth = rpoDepth st + 1})+ result <- action+ modify (\st -> st{rpoDepth = rpoDepth st - 1})+ return result+++cached :: (Eq (oc Op), Hashable (oc Op)) => CacheKey oc -> RMonad oc (oc Op) -> RMonad oc (oc Op)+cached key@(_,_,t1,t2) 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)})+ 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)++rpoMul :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op (MultiSet RuntimeTerm) (RMonad oc)+rpoMul = multisetOrder rpo'++rpo' :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RuntimeTerm (RMonad oc)+rpo' impl _ oc _ _ | oc == unsatisfiable impl = return $ unsatisfiable impl+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 t@(App f ts) u@(App g us) = incDepth result+ where+ traceString depth = printf "%s %s %s %s" (take depth $ repeat '.') (show t) (show r) (show u)+ cs' = noConstraints oc -- relevantConstraints oc cs (ops t) (ops u)+ result = cached (cs, r, t, u) $ (intersect oc cs <$> result')+ result' = cached (cs', r, t, u) $ do+ depth <- gets rpoDepth+ trace' (traceString depth) $+ if r == EQ+ then rpoMul oc r (addConstraint oc (f =. g) cs') ts us+ else+ unionAll oc <$> sequence [+ rpoMul oc GT (addConstraint oc (f >. g) cs') (MS.singleton t) us+ , rpoMul oc r (addConstraint oc (f =. g) cs') ts us+ , rpoMul oc GTE cs' ts (MS.singleton u)+ ]++++rpoGTE t u = runIdentity $ rpoGTE' ?impl (noConstraints ?impl) t u++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)+ | opGT ordering f g+ = synGTM ordering (MS.singleton t) us+synGTE' ordering (App f ts) (App g us)+ | opEQ ordering f g+ = synGTEM ordering ts us+synGTE' ordering (App _ ts) u = synGTEM ordering ts (MS.singleton u)++rpoT :: OpOrdering -> RuntimeTerm -> RuntimeTerm -> Bool+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+ (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+ ([] , [] ) -> False+ (xs', ys') -> all (\y -> any (\x -> rpoT ordering x y) xs') ys'
+ src/Language/REST/Rest.hs view
@@ -0,0 +1,188 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE NamedFieldPuns #-}++module Language.REST.Rest (+ rest+ , pathsResult+ , termsResult+ , terms+ , PathsResult(..)+ , WorkStrategy(..)+ , RESTParams(..)+ ) where++import Control.Monad+import Control.Monad.List+import Data.Hashable+import qualified Data.HashSet as S+import qualified Data.List as L+import qualified Data.HashMap.Strict as M+import qualified Data.Maybe as Mb+import Debug.Trace+import Text.Printf++import Language.REST.AbstractOC as AC+import Language.REST.RewriteRule+import Language.REST.Path+import Language.REST.Types+import Language.REST.ExploredTerms as ET+import Language.REST.WorkStrategy++newtype PathsResult rule term oc = PathsResult (S.HashSet (Path rule term oc))++newtype TermsResult rule term oc = TermsResult (S.HashSet term)++pathsResult = PathsResult S.empty+termsResult = TermsResult S.empty++class RESTResult a where+ includeInResult :: (Hashable oc, Eq oc, Hashable rule, Eq rule, Hashable term, Eq term) => Path rule term oc -> a rule term oc -> a rule term oc+ terms :: (Eq term, Hashable term) => a rule term oc -> S.HashSet term++instance RESTResult PathsResult where+ includeInResult p (PathsResult s) = PathsResult (S.insert p s)+ terms (PathsResult s) = S.fromList (concatMap pathTerms $ S.toList s)+++instance RESTResult TermsResult where+ includeInResult p (TermsResult s) = TermsResult (S.union s (S.fromList $ pathTerms p))+ terms (TermsResult s) = s+++data RESTState m rule term oc et rtype = RESTState+ { finished :: rtype rule term oc+ , working :: [Path rule term oc]+ , explored :: ExploredTerms et oc m+ , targetPath :: Maybe (Path rule term oc)+ }++data RESTParams m rule term oc et rtype = RESTParams+ { re :: S.HashSet rule+ , ru :: S.HashSet rule+ , toET :: term -> et+ , target :: Maybe term+ , workStrategy :: WorkStrategy rule term et oc+ , ocImpl :: AbstractOC oc term m+ , initRes :: rtype rule term oc+ }++rest :: forall m rule term oc et rtype .+ ( MonadIO m+ , RewriteRule m rule term+ , Show et+ , Hashable term+ , Eq term+ , Hashable rule+ , Hashable et+ , Hashable oc+ , Eq rule+ , Eq et+ , Eq oc+ , Show oc+ , RESTResult rtype)+ => RESTParams m rule term oc et rtype+ -> term+ -> m ((rtype rule term oc), Maybe (Path rule term oc))+rest RESTParams{re,ru,toET,ocImpl,workStrategy,initRes,target} t =+ rest' (RESTState initRes [([], PathTerm t S.empty)] initET Nothing)+ where+ (WorkStrategy ws) = workStrategy+ initET = ET.empty $ EF (AC.union ocImpl) (AC.notStrongerThan ocImpl)++ rest' (RESTState fin [] _ targetPath) = return (fin, targetPath)+ rest' state@(RESTState _ paths et (Just targetPath))+ | ((steps, _), remaining) <- ws paths toET et+ , length steps >= length (fst targetPath)+ = rest' state{working = remaining}+ rest' state@(RESTState fin paths et targetPath) = do+ se <- shouldExplore (toET t) lastOrdering et+ if se+ then do+ evalRWs <- candidates re -- trace ("Explore " ++ (show $ toET t)) $ candidates re+ userRWs <- candidates ru+ acceptedUserRWs <- accepted userRWs+ go evalRWs userRWs acceptedUserRWs+ else+ rest' (state{ working = remaining })+ where++ (path@(ts, PathTerm t _), remaining) = ws paths toET et++ lastOrdering :: oc+ lastOrdering = if L.null ts then top ocImpl else ordering $ last ts++ tsTerms :: [term]+ tsTerms = pathTerms path++ liftSet :: S.HashSet a -> ListT m a+ liftSet s = ListT $ return $ S.toList s++ candidates :: S.HashSet rule -> m (S.HashSet (term, rule))+ candidates rules = fmap S.fromList res+ where+ res :: m [(term, rule)]+ res = runListT $ do+ r <- liftSet rules+ t' <- ListT $ S.toList <$> apply t 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'+ ok <- lift $ isSat ocImpl ord+ guard ok+ return (t', ord))++ go evalRWs userRWs acceptedUserRewrites =+ do+ ep <- evalPaths+ up <- userPaths+ rest' (state' (ep ++ up))+ where++ state' p' = state+ { working = p' ++ remaining+ , finished = if null p' then includeInResult (ts, pt) fin else fin+ , explored =+ let+ deps = S.map (toET . fst) (S.union evalRWs userRWs)+ in+ ET.insert (toET t) lastOrdering deps et+ , targetPath =+ if Just t == target then+ case targetPath of+ Just (tp, _) | length tp <= length ts -> targetPath+ _ -> Just (ts, pt)+ else+ targetPath+ }+++ pt = PathTerm t rejectedUserRewrites++ rejectedUserRewrites :: S.HashSet (term, rule)+ rejectedUserRewrites = S.fromList $ do+ (t', r) <- S.toList userRWs+ guard $ L.notElem t' tsTerms+ guard $ Mb.isNothing $ M.lookup t' acceptedUserRewrites+ return (t', r)+++ evalPaths = runListT $ do+ (t', r) <- ListT $ return (S.toList evalRWs)+ guard $ L.notElem t' tsTerms+ let ord = refine ocImpl lastOrdering t t'+ lift (shouldExplore (toET t') ord et) >>= guard+ return (ts ++ [Step pt r ord True], PathTerm t' S.empty)++ userPaths = runListT $ do+ (t', r) <- liftSet userRWs+ ord <- ListT $ return $ Mb.maybeToList $ M.lookup t' acceptedUserRewrites+ lift (shouldExplore (toET t') ord et) >>= guard+ return (ts ++ [Step pt r ord False], PathTerm t' S.empty)
+ src/Language/REST/Rewrite.hs view
@@ -0,0 +1,56 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}++module Language.REST.Rewrite where++import GHC.Generics (Generic)++import Control.Monad.Identity+import Data.Hashable+import qualified Data.HashMap.Strict as M+import qualified Data.HashSet as S+import Text.Printf++import Language.REST.RewriteRule+import Language.REST.MetaTerm as MT+import Language.REST.RuntimeTerm+++data Rewrite = Rewrite MetaTerm MetaTerm (Maybe String)+ deriving (Eq, Ord, Generic, Hashable, Show)++type Subst = M.HashMap String RuntimeTerm++getName (Rewrite t u n) = n+named (Rewrite t u _) n = Rewrite t u (Just n)++subst :: Subst -> MetaTerm -> RuntimeTerm+subst s (MT.Var v) | Just t <- M.lookup v s = t+ | otherwise+ = error $ printf "No value for metavar %s during subst %s" (show v) (show s)+subst s (MT.RWApp op xs) = App op (map (subst s) xs)++unifyAll :: Subst -> [(MetaTerm, RuntimeTerm)] -> Maybe Subst+unifyAll su [] = Just su+unifyAll su ((x, y) : ts)+ | Just s <- unify x y su+ = unifyAll s ts+ | otherwise+ = Nothing++unify :: MetaTerm -> RuntimeTerm -> Subst -> Maybe Subst+unify (MT.Var s) term su | M.lookup s su == Just term+ = Just su+unify (MT.Var s) term su | M.lookup s su == Nothing+ = Just $ M.insert s term su+unify (MT.RWApp o1 xs) (App o2 ys) su | o1 == o2 && length xs == length ys =+ unifyAll su (zip xs ys)+unify _ _ _ = Nothing++instance Monad m => RewriteRule m Rewrite RuntimeTerm where+ apply t (Rewrite left right _) = return $ S.unions $ map go (subTerms t)+ where+ go (t', tf) | Just su <- unify left t' M.empty = S.singleton (tf $ subst su right)+ go _ | otherwise = S.empty
+ src/Language/REST/RewriteRule.hs view
@@ -0,0 +1,8 @@+{-# LANGUAGE MultiParamTypeClasses #-}++module Language.REST.RewriteRule where++import qualified Data.HashSet as S++class RewriteRule m rule term where+ apply :: term -> rule -> m (S.HashSet term)
+ src/Language/REST/RuntimeTerm.hs view
@@ -0,0 +1,39 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveAnyClass #-}++module Language.REST.RuntimeTerm where++import Data.Hashable+import GHC.Generics (Generic)+import Text.Printf+import qualified Data.List as L++import Language.REST.Op++data RuntimeTerm = App Op [RuntimeTerm] deriving (Eq, Ord, Generic, Hashable)++instance Show RuntimeTerm where+ show (App op []) = show op+ show (App op ts) = printf "%s(%s)" (show op) $ L.intercalate ", " (map show ts)++class ToRuntimeTerm a where+ toRuntimeTerm :: a -> RuntimeTerm++instance ToRuntimeTerm Op where+ toRuntimeTerm op = App op []++instance ToRuntimeTerm RuntimeTerm where+ toRuntimeTerm = id++subTerms :: RuntimeTerm -> [(RuntimeTerm, (RuntimeTerm -> RuntimeTerm))]+subTerms t@(App f ts) = (t, id) : concatMap st [0..length ts - 1]+ where+ st :: Int -> [(RuntimeTerm, (RuntimeTerm -> RuntimeTerm))]+ st i =+ let+ t = ts !! i+ go t' =+ App f $ take i ts ++ [t'] ++ drop (i + 1) ts+ go2 (st, toFull) = (st, go . toFull)+ in+ map go2 (subTerms t)
+ src/Language/REST/SMT.hs view
@@ -0,0 +1,109 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE OverloadedStrings #-}++module Language.REST.SMT where++import Control.Monad.IO.Class+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 GHC.IO.Handle++newtype SMTVar = SMTVar T.Text deriving (Eq, Ord)++data SMTExpr a where+ And :: [SMTExpr Bool] -> SMTExpr Bool+ Or :: [SMTExpr Bool] -> SMTExpr Bool+ Equal :: [SMTExpr a] -> SMTExpr Bool+ Greater :: SMTExpr Int -> SMTExpr Int -> SMTExpr Bool+ Implies :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool+ Var :: SMTVar -> SMTExpr a++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+vars (Implies e1 e2) = S.union (vars e1) (vars e2)++data SMTCommand = SMTAssert (SMTExpr Bool) | DeclareVar SMTVar | CheckSat | Push | Pop++smtFalse = Or []+smtTrue :: SMTExpr Bool+smtTrue = And []++app op trms = T.concat $ ["(", op, " ", (T.intercalate " " (map exprString trms)), ")"]++exprString :: SMTExpr a -> T.Text+exprString (And []) = "true"+exprString (Or []) = "false"+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 (Var (SMTVar var)) = var++commandString (SMTAssert expr) = app "assert" [expr]+commandString (DeclareVar (SMTVar 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+ varDecls = map DeclareVar $ S.toList (vars expr)++type SolverHandle = (Handle, Handle)++spawnZ3 = do+ (Just stdIn, Just stdOut, _, _) <- createProcess (proc "z3" ["-in"]) {std_in = CreatePipe, std_out = CreatePipe}+ return (stdIn, stdOut)++killZ3 (stdIn, _) = hClose stdIn++withZ3 f =+ do+ z3 <- liftIO $ spawnZ3+ result <- f z3+ liftIO $ killZ3 z3+ return result++checkSat' :: (Handle, Handle) -> SMTExpr Bool -> IO Bool+checkSat' (stdIn, stdOut) expr = do+ hPutStr stdIn prog+ hFlush stdIn+ result <- hGetLine stdOut+ return $ case result of+ "sat" -> True+ "unsat" -> False+ other -> error other+ where+ prog = (T.unpack $ (T.intercalate "\n" (map commandString $ askCmds expr))) ++ "\n"++checkSat :: SMTExpr Bool -> IO Bool+checkSat expr = do+ z3 <- spawnZ3+ result <- checkSat' z3 expr+ killZ3 z3+ return result++class ToSMTVar a b | a -> b where+ toSMTVar :: a -> SMTVar++class ToSMT a b where+ toSMT :: a -> SMTExpr b++instance {-# OVERLAPPABLE #-} (ToSMTVar a b) => ToSMT a b where+ toSMT :: a -> SMTExpr b+ toSMT op = Var $ toSMTVar op
+ src/Language/REST/Types.hs view
@@ -0,0 +1,79 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}++module Language.REST.Types (+ prettyPrint+ , PPArgs(..)+ , Relation(..)+ , toOrderedSet+ ) where++import GHC.Generics (Generic)+import Prelude hiding (GT, EQ)++import Data.Hashable+import qualified Data.List as L+import qualified Data.HashSet as S+import qualified Data.Set as OS+import qualified Data.Map as M+import qualified Data.Text as T+import Text.Printf++import Language.REST.Op+import Language.REST.MetaTerm as MT+import Language.REST.RuntimeTerm as MT++data PPArgs = PPArgs+ { ppReplace :: [(T.Text, T.Text)]+ , ppInfixOps :: [(T.Text, T.Text)]+ , ppCustom :: MetaTerm -> Maybe T.Text+ }++prettyPrint :: ToMetaTerm a => PPArgs -> a -> String+prettyPrint (PPArgs substs infixOps custom) t = T.unpack $ go $ replaceAll $ toMetaTerm t where++ replace s | Just (from, to) <- L.find ((`T.isPrefixOf` s) . fst) substs+ = T.append to $ T.drop (T.length from) s+ replace s | otherwise = s++ replaceAll :: MT.MetaTerm -> MT.MetaTerm+ replaceAll (MT.Var x) = MT.Var x+ replaceAll (MT.RWApp (Op op) ts) = MT.RWApp (Op (replace op)) (map replaceAll ts)++++ go :: MT.MetaTerm -> T.Text+ go (MT.Var x) = T.pack x+ go t | Just s <- custom t = 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++ needsParens (MT.RWApp (Op op) _) = op `elem` (map fst infixOps)+ needsParens _ = False++data Relation = GT | GTE | EQ deriving (Eq, Generic, Hashable)++instance Show Relation where+ show GT = ">"+ show GTE = "≥"+ show EQ = "≅"++instance Hashable a => Hashable (OS.Set a) where+ hashWithSalt i s = hashWithSalt i (OS.toList s)++instance (Hashable a, Hashable b) => Hashable (M.Map a b) where+ hashWithSalt i s = hashWithSalt i (M.toList s)++toOrderedSet :: (Eq a, Hashable a, Ord a) => S.HashSet a -> OS.Set a+toOrderedSet = OS.fromList . S.toList
+ src/Language/REST/WQO.hs view
@@ -0,0 +1,329 @@+{-# 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/WorkStrategy.hs view
@@ -0,0 +1,37 @@+{-# 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 view
@@ -0,0 +1,34 @@+{-# 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 view
@@ -0,0 +1,151 @@+{-# 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 view
@@ -0,0 +1,44 @@+{-# 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 view
@@ -0,0 +1,141 @@+{-# 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 view
@@ -0,0 +1,99 @@+{-# 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 view
@@ -0,0 +1,29 @@+{-# 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/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.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/MultisetOrder.hs view
@@ -0,0 +1,35 @@+module MultisetOrder where++import Prelude hiding (GT)+++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.Types++compareChar :: ConstraintGen impl Char Char Identity+compareChar impl r oc c1 c2 = Identity $ intersectRelation impl oc (c1, c2, r)++existingOC = OC.intersectRelation strictOC' SC.noConstraints ('a', 'c', GTE)++ms = multisetOrder compareChar strictOC' GTE++multisetNext = ms existingOC (M.fromList "bac") (M.fromList "aaaa")++unsat :: Identity (StrictOC Char)+unsat = do+ mn <- multisetNext+ return $ OC.intersectRelation strictOC' mn ('c', 'a', GT)++tests :: [(String, Bool)]+tests = [+ ("Constraints",+ (SC.noConstraints /=+ (runIdentity $ ms SC.noConstraints (M.fromList "bc") (M.fromList "aa"))))+ , ("Unsat", SC.isUnsatisfiable $ runIdentity unsat)+ ]
+ test/OpOrdering.hs view
@@ -0,0 +1,32 @@+{-# LANGUAGE OverloadedStrings #-}++module OpOrdering where++import Language.REST.Op+import Language.REST.OpOrdering+import Language.REST.WQO+import Data.Maybe as Mb++tests = [+ ("parse",+ fromJust (+ parseOO "cons = z ∧ g = nil ∧ h = s ∧ cons > g ∧ cons > h ∧ h > f ∧ h > g"+ ) == wqo)+ ,("minimal",+ fromJust (+ parseOO "f > + ^ g > z ^ + = cons ^ cons > z ^ f = g"+ ) ==+ fromJust (+ parseOO "f > + ^ + = cons ^ cons > z ^ f = g"+ )+ ) ]+ where++ Just wqo = mergeAll [ ("cons" =. "z")+ , ("g" =. "nil")+ , ("h" =. "s")+ , ("cons" >. "g")+ , ("cons" >. "h")+ , ("h" >. "f")+ , ("h" >. "g")+ ]
+ test/QuickCheckTests.hs view
@@ -0,0 +1,153 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE OverloadedStrings #-}+module QuickCheckTests where++import Test.QuickCheck+import Test.QuickCheck.Monadic++import Control.Monad.Identity+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.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 = [+ ("f", 3)+ , ("g", 2)+ , ("h", 1)+ , ("s", 1)+ , ("z", 0)+ , ("+", 2)+ , ("cons", 2)+ , ("nil", 0)+ ]++gen_op :: Gen Op+gen_op =+ oneof (map (return . Op . fst) syms)++gen_po :: Gen (PO.PartialOrder Op)+gen_po =+ do+ num_ops <- choose (0, 10)+ go PO.empty num_ops+ where+ go :: PO.PartialOrder Op -> Int -> Gen (PO.PartialOrder Op)+ go po 0 = return po+ go po n = do+ f <- gen_op+ g <- gen_op+ let po' = fromMaybe po $ PO.insert po f g+ go po' (n - 1)++gen_wqo_steps :: Gen ([(Op, Op, WQO.QORelation)])+gen_wqo_steps =+ do+ numOps <- choose (0, 10)+ vectorOf numOps go+ where+ go = do+ f <- gen_op+ g <- gen_op+ r <- arbitrary+ return (f, g, r)++toWQO :: [(Op, Op, WQO.QORelation)] -> WQO Op+toWQO = go WQO.empty where+ go wqo [] = wqo+ go wqo ((f, g, r):xs) =+ let+ wqo' = fromMaybe wqo $ WQO.insertMaybe wqo (f, g, r)+ in+ go wqo' xs++gen_wqo :: Gen (WQO Op)+gen_wqo = fmap toWQO gen_wqo_steps++gen_term :: Gen RuntimeTerm+gen_term = sized go+ where+ go :: Int -> Gen RuntimeTerm+ go sz = do+ (op, arity) <- oneof $ map return $ (filter ((<= sz) . snd) syms)+ args <- vectorOf arity (go (sz `div` (arity + 1)))+ return $ App (Op op) args++instance Arbitrary WQO.QORelation where+ arbitrary = oneof [return WQO.QGT, return WQO.QEQ]++instance Arbitrary Op where+ arbitrary = gen_op++instance Arbitrary RuntimeTerm where+ arbitrary = gen_term++instance Arbitrary (PO.PartialOrder Op) where+ arbitrary = gen_po++instance Arbitrary (WQO Op) where+ arbitrary = gen_wqo++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+ where+ gte f g = Mb.isJust $ WQO.getRelation wqo f g+ types = f::Op++prop_rpoTrans t u v wqo = synGTE wqo t u && synGTE wqo u v ==> synGTE wqo t v++prop_rpoCons impl t u = monadicIO $ do+ isSat <- run $ OC.isSatisfiable impl constraints+ pre isSat+ assert $ synGTE ordering t u+ where+ constraints = rpoGTE t u+ ordering = Mb.fromJust (OC.getOrdering impl constraints)++prop_permits steps = SC.permits (SC.noConstraints) (toWQO steps)++-- Should fail+-- If this prop was true, we'd only ever need to check each term once+-- Generated counterexample:+-- f(s(z), h(nil), nil) -> cons(s(z), z) -> h(nil + z) \-> s(nil) + h(nil)+-- f(s(z), h(nil), nil) -> s(nil) + h(nil) -> h(nil + z) -> s(nil) + h(nil)+-- prop_rpot2 t0 t1 t2 t3 u1 = monadicIO $ do+-- pre <$> run (canOrient [t0, t1, t2])+-- pre <$> run (canOrient [t0, u1, t2, t3])+-- assert <$> run (canOrient [t0, t1, t2, t3])+-- where+-- types = t0::RuntimeTerm++tests = sequence+ [+ -- quickCheckWith stdArgs{maxDiscardRatio = 1000} prop_rpot2+ quickCheckWith stdArgs prop_permits+ , quickCheckWith stdArgs{maxDiscardRatio = 1000} prop_poTrans+ , quickCheckWith stdArgs{maxDiscardRatio = 100} prop_wqoTrans+ , putStrLn "Transitivity of RPO:"+ , quickCheckWith stdArgs{maxDiscardRatio = 100} prop_rpoTrans+ , putStrLn "RPO aligns with concrete:"+ , quickCheckWith stdArgs{maxSize = 10, maxSuccess = 20, maxDiscardRatio = 100} (prop_rpoCons ?impl)+ ]+ where+ ?impl = LC.lazyOC
+ test/RPO.hs view
@@ -0,0 +1,71 @@+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE OverloadedStrings #-}++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.RuntimeTerm+import Language.REST.RPO+import Language.REST.WQO++import Data.Maybe as Mb++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 = "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 = "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 = "concat(ite(isNil(ysaLe), Nil, concat(reverse(lqdcselectcons2(ysaLe)), cons(lqdcselectcons1(ysaLe), Nil))), concat(reverse(lqdcselectcons2(dsdOz)), cons(lqdcselectcons1(dsdOz), Nil)))"++listsRight = "concat(concat(ite(isNil(ysaLe), Nil, concat(reverse(lqdcselectcons2(ysaLe)), cons(lqdcselectcons1(ysaLe), Nil))), reverse(lqdcselectcons2(dsdOz))), cons(lqdcselectcons1(dsdOz), Nil))"++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 = "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 = [+ "concat(flatten(la1Bz), concat(flatten(ra1BA), nsa1By))",+ "concat(ite(isLeaf(la1Bz), cons(LeaflqdcselectLeaf1(la1Bz), nil), concat(flatten(NodelqdcselectNode1(la1Bz)), flatten(NodelqdcselectNode2(la1Bz)))), concat(ite(isLeaf(ra1BA), cons(LeaflqdcselectLeaf1(ra1BA), nil), concat(flatten(NodelqdcselectNode1(ra1BA)), flatten(NodelqdcselectNode2(ra1BA)))), nsa1By))",+ "concat(concat(ite(isLeaf(la1Bz), cons(LeaflqdcselectLeaf1(la1Bz), nil), concat(flatten(NodelqdcselectNode1(la1Bz)), flatten(NodelqdcselectNode2(la1Bz)))), ite(isLeaf(ra1BA), cons(LeaflqdcselectLeaf1(ra1BA), nil), concat(flatten(NodelqdcselectNode1(ra1BA)), flatten(NodelqdcselectNode2(ra1BA))))), nsa1By)"+ ]++rpoSeq xs = go (OC.noConstraints ?impl) xs where+ go c (t:u:xs) = OC.intersect ?impl c (rpoGTE t u)+ go c _ = c+++tests :: (Hashable (oc Op), Eq (oc Op), Show (oc Op)) => (?impl :: OrderingConstraints oc IO) => [(String, IO Bool)]+tests =+ let+ f = Op "f"+ g = Op "g"+ h = Op "h"+ in+ [ ("RPO1", return $ (rpoGTE "f(z)" "g(s(z))")+ == OC.intersect ?impl (OC.singleton ?impl (f >. g)) (OC.singleton ?impl (f >. s)))+ , ("RPO2", isUnsatisfiable ?impl $+ OC.intersect ?impl+ (rpoGTE "f(z)" "g(s(z))")+ (rpoGTE "g(s(z))" "f(h(z))"))+ , ("RPO3", isSatisfiable ?impl (rpoGTE bigLeft bigRight))+ , ("RPO4", isUnsatisfiable ?impl (rpoGTE massiveLeft massiveRight))+ , ("RPO5", isSatisfiable ?impl (rpoGTE listsLeft listsRight))+ , ("RPO6", isSatisfiable ?impl (rpoGTE flattenLeft2 flattenRight2))+ , ("RPOOrient", isUnsatisfiable ?impl $ rpoSeq flattenSeq)+ , ("SynGTE", return $ synGTE OpOrdering.empty (App s [App s [App g [App (Op "+") [App h [App s [App z []]],App z []],App s [App s [App g [App z [],App z []]]]]]]) (App z []))+ , ("SynGTE2",+ return $ synGTE (Mb.fromJust $ mergeAll [+ ("cons" >. g)+ , (f >. s)+ , (h >. g)+ , (h >. "nil")]) "s(cons(h(h(z)), f(nil, nil, z)))" "g(z, cons(g(nil, nil), s(s(z))))")+ ]
+ test/StrictOC.hs view
@@ -0,0 +1,24 @@+{-# LANGUAGE OverloadedStrings #-}+module StrictOC where++import Data.Maybe++import Language.REST.OrderingConstraints.Strict+import Language.REST.WQO+import Language.REST.Op+import DSL+import Language.REST.OpOrdering++tests =+ [+ ("permits", permits noConstraints wqo)+ , ("permits2", permits noConstraints $ fromJust $ parseOO "+ = f = nil = s ∧ + > g ∧ + > h ∧ cons > + ∧ cons > g")+ ] where+ Just wqo = mergeAll [ ("cons" =. "z")+ , ("g" =. "nil")+ , ("h" =. "s")+ , ("cons" >. "g")+ , ("cons" >. "h")+ , ("h" >. "f")+ , ("h" >. "g")+ ]
+ test/Test.hs view
@@ -0,0 +1,227 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE OverloadedStrings #-}++module Main where++import Data.Hashable+import Control.Monad.Identity+import qualified Arith as A+import qualified Data.HashMap.Strict as M+import OpOrdering+import DSL+import WQO as WQO+import MultisetOrder as MultisetOrder+import Nat+import RPO as RPO+import StrictOC as StrictOC+import LazyOC as LazyOC+import qualified QuickCheckTests as QuickCheckTests+import System.IO+import Language.REST.AbstractOC+import Language.REST.OCToAbstract+import Language.REST.Core+import Language.REST.OrderingConstraints as OC+import Language.REST.Op+import Language.REST.RPO+import Language.REST.OpOrdering+import Language.REST.RuntimeTerm+import Language.REST.MetaTerm as MT+import Language.REST.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 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)++rewrites :: (Show oc, Hashable oc, Eq oc)+ => (?impl :: AbstractOC oc RuntimeTerm IO)+ => S.HashSet Rewrite -> S.HashSet Rewrite -> RuntimeTerm -> IO (S.HashSet RuntimeTerm)+rewrites evalRWs userRWs t0 =+ terms <$> fst <$> rest+ RESTParams+ { re = evalRWs+ , ru = userRWs+ , toET = id+ , target = Nothing+ , workStrategy = notVisitedFirst+ , ocImpl = ?impl+ , initRes = termsResult+ } t0++runTest :: (String, IO Bool) -> IO ()+runTest (name, test) = do+ putStr $ "Running " ++ name ++ "... "+ hFlush stdout+ ok <- test+ if ok+ then putStrLn "Passed"+ else error $ "Test " ++ name ++ " FAILED"++class Testable a where+ toTest :: a -> IO Bool++instance Testable Bool where+ toTest = return++instance Testable (IO Bool) where+ toTest = id++runTestSuite :: Testable a => String -> [(String, a)] -> IO ()+runTestSuite name tests = do+ putStrLn $ "Running test suite: " ++ name+ mapM_ (runTest . go) tests+ where+ go (name, test) = (name, toTest test)+++orderingTests :: (Hashable (oc Op), Show (oc Op), Ord (oc Op)) => (?impl :: OrderingConstraints oc IO) => [(String, IO Bool)]+orderingTests =+ [+ ("simple1", return $ not $ (rpoGTE "f(t1)" "g(t2)") `permits'` (t1Op =. t2Op))+ , ("simple2", return $ (rpoGTE "f(t1)" "g(t2)") `permits'` (Mb.fromJust $ merge (f >. g) (t1Op =. t2Op)))+ , ("simple3", return $ (rpoGTE "f(t1)" "g(t2)") `permits'` (Mb.fromJust $ merge (f >. g) (t1Op >. t2Op)))+ , ("subterm", return $ rpoGTE "f(g)" "f" == noConstraints ?impl)+ , ("intersect", OC.isUnsatisfiable ?impl $ OC.intersect ?impl (OC.singleton ?impl (f >. g)) (OC.singleton ?impl (g >. f)))+ ]+ where+ permits' = permits ?impl++proveEQ :: (Show oc, Hashable oc, Eq oc) => (?impl :: AbstractOC oc RuntimeTerm IO)+ => S.HashSet Rewrite -> S.HashSet Rewrite -> RuntimeTerm -> RuntimeTerm -> IO Bool+proveEQ evalRWs userRWs have want =+ do+ rw1 <- (rewrites evalRWs userRWs have)+ rw2 <- (rewrites 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 =+ [+ ("Contains", return $ contains (intToTerm 2) (intToTerm 1))+ , ("Diverge", not <$> (diverges [ (intToTerm 2) .+ t1+ , (intToTerm 1) .+ t1+ ]+ ))+ , ("Diverge3", not <$> (diverges [ (t1 .+ t2) .+ t3+ , t1 .+ (t2 .+ t3)+ , (t2 .+ t3) .+ t1+ ]+ ))+ , ("Eval1", arithEQ (intToTerm 2 .+ intToTerm 3) 5)+ , ("Eval2", arithEQ (ack (intToTerm 3) (intToTerm 2)) 29)+ , ("Subst1", return $ subst (M.fromList [("x", intToTerm 1), ("y", intToTerm 2)]) (x #+ y) == (intToTerm 1 .+ intToTerm 2))+ , ("ArithTerm", termTest)+ , ("ArithTerm2", termTest2)+ , ("Arith0", eq (t1 .+ t2 .+ intToTerm 1) (t1 .+ (intToTerm 1 .+ t2)))+ , ("Arith1", eq (intToTerm 2 .+ intToTerm 3) (intToTerm 3 .+ intToTerm 2))+ , ("Arith2", eq (t1 .+ t2) (t2 .+ t1))+ , ("Arith3", not <$> eq (t2 .+ t1) (t2 .+ t2))+ , ("Arith4", eq ((t1 .+ t2) .+ t3) (t1 .+ (t2.+ t3)))+ , ("Arith4.1", eq (t1 .+ t2 .+ t3) (t3 .+ t2 .+ t1))+ , ("Arith5", eq (zero .+ t1) t1)+ , ("Arith5.1", eq (zero .+ zero .+ t1) t1)+ , ("Arith5.2", eq (zero .+ zero .+ zero .+ t1) t1)+ , ("Arith6", eq (((t1 .+ t1) .+ t3) .+ t4) (t1 .+ (t1 .+ (t3 .+ t4))))+ , ("Arith7", eq ((intToTerm 2 .+ intToTerm 1) .+ t1) (intToTerm 2 .+ (intToTerm 1 .+ t1)))+ ]+ where++ arithEQ t n = do+ t' <- eval A.evalRWs t+ return $ termToInt t' == Just n+++ termTest = proveEQ evalRWs userRWs (App f [t1]) zero+ where+ evalRWs = S.union termEvalRWs A.evalRWs+ userRWs = S.insert (MT.RWApp g [x] ~> MT.RWApp f [x]) A.userRWs+ termEvalRWs = S.fromList+ [ MT.RWApp f [x] ~> MT.RWApp g [suc' x]+ , MT.RWApp g [x] ~> zero'+ ]+ f = Op "f"+ g = Op "g"++ termTest2 = proveEQ evalRWs userRWs (App f [zero]) (App g [zero])+ where+ evalRWs = S.union termEvalRWs A.evalRWs+ userRWs = S.insert (MT.RWApp f [x] ~> MT.RWApp g [(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'+ ]+ f = Op "f"+ g = Op "g"+++ eq = proveEQ 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 []])+ , ("Complete1" , eq (App start []) (App finish []))+ , ("EvalComplete2" , (== (App finish [])) <$> eval completeUserRWs (App start' [App s1 []]) )+ , ("Complete2" , eq (App start' [App s1 []]) (App finish []))+ ]+ where++ completeUserRWs = S.fromList+ [ MT.RWApp start [] ~> MT.RWApp mid []+ , MT.RWApp mid [] ~> MT.RWApp finish []++ , MT.RWApp start' [MT.RWApp s2 []] ~> MT.RWApp mid' [MT.RWApp s1 []]+ , MT.RWApp s1 [] ~> MT.RWApp s2 []+ , MT.RWApp mid' [MT.RWApp s2 []] ~> MT.RWApp finish []+ ]++ eq :: RuntimeTerm -> RuntimeTerm -> IO Bool+ eq = proveEQ S.empty completeUserRWs++ start = Op "start"+ mid = Op "mid"+ finish = Op "finish"++ start' = Op "start'"+ mid' = Op "mid'"++ s1 = Op "s1"+ s2 = Op "s2"++ocTests z3 = do+ runTestSuite "LazyOC" LazyOC.tests+ runTestSuite "StrictOC" StrictOC.tests+ runTestSuite "RPO" RPO.tests+ runTestSuite "Ordering" orderingTests+ where+ ?impl = AC.adtOC z3++main :: IO ()+main = spawnZ3 >>= go where+ go z3 =+ do+ putStrLn "Running REST Test Suite"+ QuickCheckTests.tests+ runTestSuite "OpOrdering" OpOrdering.tests+ ocTests z3+ runTestSuite "MultisetOrder" MultisetOrder.tests+ runTestSuite "WQO" WQO.tests+ runTestSuite "Arith" arithTests+ runTestSuite "Complete" completeTests+ killZ3 z3+ where+ ?impl = lift (AC.adtOC z3) rpo
+ test/WQO.hs view
@@ -0,0 +1,18 @@+module WQO where++import Language.REST.WQO as WQO++basicInvalid :: Maybe (WQO Char)+basicInvalid = do+ wqo1 <- WQO.singleton ('A', 'C', QGT)+ WQO.insertMaybe wqo1 ('C', 'A', QGT)++tests :: [(String, Bool)]+tests =+ let+ ValidExtension fg = insert empty ("f", "g", QGT)+ ValidExtension fgyz = insert fg ("y", "z", QGT)+ in+ [ ("NotStrongerThan", fg `notStrongerThan` fgyz)+ , ("RejectInvalid", basicInvalid == Nothing)+ ]