{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE NamedFieldPuns #-} module Language.REST.KBO (kbo, kboGTE) where import Language.REST.OCAlgebra import Language.REST.Op import Language.REST.RuntimeTerm as RT import Language.REST.SMT import Language.REST.Internal.Util import qualified Data.Map as M termOps :: RuntimeTerm -> [Op] termOps :: RuntimeTerm -> [Op] termOps (App Op f [RuntimeTerm] xs) = Op fOp -> [Op] -> [Op] forall a. a -> [a] -> [a] :((RuntimeTerm -> [Op]) -> [RuntimeTerm] -> [Op] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap RuntimeTerm -> [Op] termOps [RuntimeTerm] xs) arityConstraints :: RuntimeTerm -> SMTExpr Bool arityConstraints :: RuntimeTerm -> SMTExpr Bool arityConstraints RuntimeTerm t = Map Op Int -> SMTExpr Bool forall a. ToSMT a Int => Map a Int -> SMTExpr Bool toExpr (Map Op Int -> SMTExpr Bool) -> Map Op Int -> SMTExpr Bool forall a b. (a -> b) -> a -> b $ Map Op Int -> RuntimeTerm -> Map Op Int go Map Op Int forall k a. Map k a M.empty RuntimeTerm t where go :: M.Map Op Int -> RuntimeTerm -> M.Map Op Int go :: Map Op Int -> RuntimeTerm -> Map Op Int go Map Op Int m (App Op f []) = Op -> Int -> Map Op Int -> Map Op Int forall k a. Ord k => k -> a -> Map k a -> Map k a M.insert Op f Int 1 Map Op Int m go Map Op Int m (App Op f [RuntimeTerm targ]) = Map Op Int -> RuntimeTerm -> Map Op Int go (Op -> Int -> Map Op Int -> Map Op Int forall k a. Ord k => k -> a -> Map k a -> Map k a M.insert Op f Int 1 Map Op Int m) RuntimeTerm targ go Map Op Int m (App Op f [RuntimeTerm] ts) = (Map Op Int -> RuntimeTerm -> Map Op Int) -> Map Op Int -> [RuntimeTerm] -> Map Op Int forall (t :: * -> *) b a. Foldable t => (b -> a -> b) -> b -> t a -> b foldl Map Op Int -> RuntimeTerm -> Map Op Int go (Op -> Int -> Map Op Int -> Map Op Int forall k a. Ord k => k -> a -> Map k a -> Map k a M.insert Op f Int 0 Map Op Int m) [RuntimeTerm] ts toExpr :: Map a Int -> SMTExpr Bool toExpr Map a Int m = [SMTExpr Bool] -> SMTExpr Bool And ([SMTExpr Bool] -> SMTExpr Bool) -> [SMTExpr Bool] -> SMTExpr Bool forall a b. (a -> b) -> a -> b $ ((a, Int) -> SMTExpr Bool) -> [(a, Int)] -> [SMTExpr Bool] forall a b. (a -> b) -> [a] -> [b] map (a, Int) -> SMTExpr Bool forall a. ToSMT a Int => (a, Int) -> SMTExpr Bool toConstraint (Map a Int -> [(a, Int)] forall k a. Map k a -> [(k, a)] M.toList Map a Int m) toConstraint :: (a, Int) -> SMTExpr Bool toConstraint (a sym, Int n) = a -> SMTExpr Int forall a b. ToSMT a b => a -> SMTExpr b toSMT a sym SMTExpr Int -> SMTExpr Int -> SMTExpr Bool `smtGTE` (Int -> SMTExpr Int Const Int n) kboGTE :: RuntimeTerm -> RuntimeTerm -> SMTExpr Bool kboGTE :: RuntimeTerm -> RuntimeTerm -> SMTExpr Bool kboGTE RuntimeTerm t RuntimeTerm u = RuntimeTerm -> SMTExpr Bool arityConstraints RuntimeTerm t SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool `smtAnd` RuntimeTerm -> SMTExpr Bool arityConstraints RuntimeTerm u SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool `smtAnd` ([Op] -> SMTExpr Int forall a. ToSMT a Int => [a] -> SMTExpr Int size [Op] tOps SMTExpr Int -> SMTExpr Int -> SMTExpr Bool `smtGTE` [Op] -> SMTExpr Int forall a. ToSMT a Int => [a] -> SMTExpr Int size [Op] uOps) where ([Op] tOps, [Op] uOps) = (Op -> Op -> Bool) -> [Op] -> [Op] -> ([Op], [Op]) forall a. Eq a => (a -> a -> Bool) -> [a] -> [a] -> ([a], [a]) removeEqBy Op -> Op -> Bool forall a. Eq a => a -> a -> Bool (==) (RuntimeTerm -> [Op] termOps RuntimeTerm t) (RuntimeTerm -> [Op] termOps RuntimeTerm u) size :: [a] -> SMTExpr Int size [a] ops = [SMTExpr Int] -> SMTExpr Int smtAdd ((a -> SMTExpr Int) -> [a] -> [SMTExpr Int] forall a b. (a -> b) -> [a] -> [b] map a -> SMTExpr Int forall a b. ToSMT a b => a -> SMTExpr b toSMT [a] ops) kbo :: SolverHandle -> OCAlgebra (SMTExpr Bool) RuntimeTerm IO kbo :: SolverHandle -> OCAlgebra (SMTExpr Bool) RuntimeTerm IO kbo SolverHandle solver = OCAlgebra :: forall c a (m :: * -> *). (c -> m Bool) -> (c -> a -> a -> c) -> c -> (c -> c -> c) -> (c -> c -> m Bool) -> OCAlgebra c a m OCAlgebra { isSat :: SMTExpr Bool -> IO Bool isSat = SolverHandle -> SMTExpr Bool -> IO Bool checkSat' SolverHandle solver , SMTExpr Bool -> RuntimeTerm -> RuntimeTerm -> SMTExpr Bool refine :: SMTExpr Bool -> RuntimeTerm -> RuntimeTerm -> SMTExpr Bool refine :: SMTExpr Bool -> RuntimeTerm -> RuntimeTerm -> SMTExpr Bool refine , top :: SMTExpr Bool top = SMTExpr Bool smtTrue , SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool union :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool union :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool union , SMTExpr Bool -> SMTExpr Bool -> IO Bool notStrongerThan :: SMTExpr Bool -> SMTExpr Bool -> IO Bool notStrongerThan :: SMTExpr Bool -> SMTExpr Bool -> IO Bool notStrongerThan } where union :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool union SMTExpr Bool e1 SMTExpr Bool e2 = [SMTExpr Bool] -> SMTExpr Bool Or [SMTExpr Bool e1, SMTExpr Bool e2] refine :: SMTExpr Bool -> RuntimeTerm -> RuntimeTerm -> SMTExpr Bool refine SMTExpr Bool e RuntimeTerm t RuntimeTerm u = SMTExpr Bool e SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool `smtAnd` RuntimeTerm -> RuntimeTerm -> SMTExpr Bool kboGTE RuntimeTerm t RuntimeTerm u notStrongerThan :: SMTExpr Bool -> SMTExpr Bool -> IO Bool notStrongerThan SMTExpr Bool e1 SMTExpr Bool e2 = SolverHandle -> SMTExpr Bool -> IO Bool checkSat' SolverHandle solver (SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool Implies SMTExpr Bool e2 SMTExpr Bool e1)