Commit 49fe742c authored by Michael Hanus's avatar Michael Hanus
Browse files

Tools adapted to new Rewriting librariesRe

parent c2c9418c
......@@ -2,10 +2,7 @@
TOOL=$(BINDIR)/currycheck
REWRITINGDIR = $(CURDIR)/../verification
# currycheck input path and dependencies:
CCPATH = $(REWRITINGDIR)
# currycheck (main) dependencies:
DEPS = *.curry $(LIBDIR)/Test/EasyCheck.curry $(LIBDIR)/AbstractCurry/*.curry
.PHONY: all compile install clean uninstall
......@@ -26,4 +23,4 @@ uninstall: clean
rm -f $(TOOL)
CurryCheck: $(DEPS)
$(REPL) $(REPL_OPTS) :set path $(CCPATH) :l CurryCheck :save :q
$(REPL) $(REPL_OPTS) :l CurryCheck :save :q
......@@ -109,6 +109,8 @@ maxSimpSteps = 100
simplifyRule :: Int -> TRS QName -> QName -> CRule -> IO CRule
simplifyRule verb simprules qn crule@(CRule rpats _) = do
(id $!! (lhs,rhs)) `seq` done -- in order to raise a fromRule error here!
unless (null trs) $
error $ "simplifyRule: cannot handle local TRS:\n" ++ showTRS snd trs
when (verb > 1 ) $ putStrLn $ unlines
["POSTCONDITION: " ++ showRule snd (lhs,rhs),
"POSTCONDEXP: " ++ showTerm snd postcondexp,
......@@ -116,11 +118,11 @@ simplifyRule verb simprules qn crule@(CRule rpats _) = do
"SIMPPOSTCOND: " ++ showRule snd simppostcond ]
return (simpleRule rpats (term2acy (concatMap varsOfPat rpats) simppostrhs))
where
(lhs,rhs) = fromRule qn crule
postcondexp = postCondition2Term lhs rhs
simpterm = simplifyTerm maxSimpSteps simprules postcondexp
simppostrhs = postConditionTermToRule lhs simpterm
simppostcond = (lhs, simppostrhs)
((lhs,rhs),trs) = fromRule qn crule
postcondexp = postCondition2Term lhs rhs
simpterm = simplifyTerm maxSimpSteps simprules postcondexp
simppostrhs = postConditionTermToRule lhs simpterm
simppostcond = (lhs, simppostrhs)
--- Transform a post-condition rule into a term by substituting
--- the last argument variable by the function call.
......@@ -165,7 +167,7 @@ simplifyTerm maxsteps simprules term =
| p <- positions term,
rule <- simprules,
let vMax = maximum (0: tVars term) + 1,
let (lhs,rhs) = renameRVars vMax rule,
let (lhs,rhs) = renameRuleVars vMax rule,
sub <- maybeToList (match (term |> p) lhs) ]
-- match t1 t2 = sub iff sub(t2) = t1
......
------------------------------------------------------------------------------
--- Library for representation and computation of critical pairs.
---
--- @author Jan-Hendrik Matthes
--- @version May 2016
--- @category algorithm
------------------------------------------------------------------------------
module Rewriting.CriticalPairs
( CPair
, showCPair, cPairs
) where
import Either (rights)
import List (maximum, nub)
import Rewriting.Position (eps, positions, (|>), replaceTerm)
import Rewriting.Rules (TRS, rVars, isVariantOf, renameRVars)
import Rewriting.Substitution (applySubst)
import Rewriting.Term (Term, showTerm, isVarTerm)
import Rewriting.Unification (unify)
-- ---------------------------------------------------------------------------
-- Representation of critical pairs
-- ---------------------------------------------------------------------------
--- A critical pair represented as a pair of terms and parameterized over the
--- kind of function symbols, e.g., strings.
type CPair f = (Term f, Term f)
-- ---------------------------------------------------------------------------
-- Pretty-printing of critical pairs
-- ---------------------------------------------------------------------------
-- \x3008 = LEFT ANGLE BRACKET
-- \x3009 = RIGHT ANGLE BRACKET
--- Transforms a critical pair into a string representation.
showCPair :: (f -> String) -> CPair f -> String
showCPair s (l, r)
= "\x3008" ++ (showTerm s l) ++ ", " ++ (showTerm s r) ++ "\x3009"
-- ---------------------------------------------------------------------------
-- Computation of critical pairs
-- ---------------------------------------------------------------------------
--- Computes the critical pairs of a term rewriting system.
cPairs :: TRS f -> [CPair f]
cPairs trs = nub [(applySubst sub r1,
replaceTerm (applySubst sub l1) p (applySubst sub r2)) |
rule1@(l1, r1) <- trs,
let vMax = (maximum (0:(rVars rule1))) + 1,
rule2@(l2, r2) <- map (renameRVars vMax) trs,
p <- positions l1,
let l1p = l1 |> p, not (isVarTerm l1p),
sub <- rights [unify [(l1p, l2)]],
p /= eps || not (isVariantOf rule1 rule2)]
\ No newline at end of file
------------------------------------------------------------------------------
--- Library to read and transform a curry program into an equivalent
--- representation where every function gets assigned the corresponding term
--- rewriting system.
---
--- @author Jan-Hendrik Matthes
--- @version May 2016
--- @category algorithm
------------------------------------------------------------------------------
module Rewriting.Files
( ConsData, TRSData, RWData
, emptyConsData, extendConsData, lookupConsData, emptyTRSData
, extendTRSData, lookupTRSData, readCurryProgram, fromCurryProg
, fromTypeDecl, fromConsDecl, fromFuncDecl, fromRule, fromPattern
, fromLiteral, fromRhs, fromExpr, showQName, readQName
) where
import AbstractCurry.Files (tryReadCurryFile)
import AbstractCurry.Types
import FiniteMap (FM, emptyFM, addToFM, lookupFM)
import Rewriting.Rules (Rule, TRS)
import Rewriting.Substitution (Subst, emptySubst, extendSubst, applySubst)
import Rewriting.Term (Term (..), tConst)
type ConsData = FM QName QName
type TRSData = FM QName (TRS QName)
type RWData = (TRSData, ConsData)
emptyConsData :: ConsData
emptyConsData = emptyFM (<)
extendConsData :: ConsData -> QName -> QName -> ConsData
extendConsData = addToFM
lookupConsData :: ConsData -> QName -> Maybe QName
lookupConsData = lookupFM
emptyTRSData :: TRSData
emptyTRSData = emptyFM (<)
extendTRSData :: TRSData -> QName -> TRS QName -> TRSData
extendTRSData = addToFM
lookupTRSData :: TRSData -> QName -> Maybe (TRS QName)
lookupTRSData = lookupFM
readCurryProgram :: String -> IO (Either String RWData)
readCurryProgram f = do res <- tryReadCurryFile f
case res of
(Left err) -> return (Left err)
(Right cp) -> return (Right (fromCurryProg cp))
fromCurryProg :: CurryProg -> RWData
fromCurryProg (CurryProg _ _ ts fs _) = (trsData, consData)
where
extendTRS :: TRSData -> [(QName, TRS QName)] -> TRSData
extendTRS = foldr (\(fn, trs) trsd -> extendTRSData trsd fn trs)
trsData = extendTRS emptyTRSData (map fromFuncDecl fs)
extendCons :: ConsData -> [(QName, QName)] -> ConsData
extendCons = foldr (\(cn, tn) consd -> extendConsData consd cn tn)
consData = extendCons emptyConsData (concatMap fromTypeDecl ts)
fromTypeDecl :: CTypeDecl -> [(QName, QName)]
fromTypeDecl (CType tn _ _ cs) = map (fromConsDecl tn) cs
fromTypeDecl (CTypeSyn _ _ _ _) = []
fromTypeDecl (CNewType tn _ _ c) = [fromConsDecl tn c]
fromConsDecl :: QName -> CConsDecl -> (QName, QName)
fromConsDecl tn (CCons cn _ _) = (cn, tn)
fromConsDecl tn (CRecord cn _ _) = (cn, tn)
fromFuncDecl :: CFuncDecl -> (QName, TRS QName)
fromFuncDecl (CFunc fn _ _ _ rs) = (fn, map (fromRule fn) rs)
fromFuncDecl (CmtFunc _ fn _ _ _ rs) = (fn, map (fromRule fn) rs)
fromRule :: QName -> CRule -> Rule QName
fromRule fn (CRule ps rhs) = (TermCons fn (map fromPattern ps), rTerm)
where
rTerm = applySubst (asSubst ps) (fromRhs rhs)
asSubst :: [CPattern] -> Subst QName
asSubst = extend emptySubst
where
extend :: Subst QName -> [CPattern] -> Subst QName
extend s [] = s
extend s (p:ps)
= case p of
(CPAs v x) -> extend (extendSubst s (fst v) (fromPattern x)) ps
_ -> extend s ps
fromPattern :: CPattern -> Term QName
fromPattern (CPVar v) = TermVar (fst v)
fromPattern (CPLit l) = fromLiteral l
fromPattern (CPComb fn ps) = TermCons fn (map fromPattern ps)
fromPattern (CPAs _ p) = fromPattern p
fromPattern (CPFuncComb fn ps) = TermCons fn (map fromPattern ps)
fromPattern (CPLazy p) = fromPattern p
fromPattern (CPRecord _ _) = error "CPRecord not supported!"
fromLiteral :: CLiteral -> Term QName
fromLiteral (CIntc i) = tConst ("%i", show i)
fromLiteral (CFloatc f) = tConst ("%f", show f)
fromLiteral (CCharc c) = tConst ("%c", [c])
fromLiteral (CStringc s) = tConst ("%s", s)
fromRhs :: CRhs -> Term QName
fromRhs (CSimpleRhs expr _) = fromExpr expr
fromRhs (CGuardedRhs _ _) = error "CGuardedRhs not supported!"
fromExpr :: CExpr -> Term QName
fromExpr (CVar v) = TermVar (fst v)
fromExpr (CLit l) = fromLiteral l
fromExpr (CSymbol s) = tConst s
fromExpr (CApply f e)
= case fromExpr f of
TermCons c ts -> TermCons c (ts ++ [fromExpr e])
TermVar _ -> error "Argument is not a function!"
fromExpr (CLambda _ _) = error "CLambda not supported!"
fromExpr (CLetDecl _ _) = error "CLetDecl not supported!"
fromExpr (CDoExpr _) = error "CDoExpr not supported!"
fromExpr (CListComp _ _) = error "CListComp not supported!"
fromExpr (CCase _ _ _) = error "CCase not supported!"
fromExpr (CTyped _ _) = error "CTyped not supported!"
fromExpr (CRecConstr _ _) = error "CRecConstr not supported!"
fromExpr (CRecUpdate _ _) = error "CRecUpdate not supported!"
--- Transforms a qualified name into a string representation.
showQName :: QName -> String
showQName (qn, fn) = if qn == ""
then fn
else qn ++ "." ++ fn
--- Transforms a string into a qualified name.
readQName :: String -> QName
readQName s = case break (== '.') s of
q@(_, []) -> q
(qn, _:fn) -> (qn, fn)
\ No newline at end of file
------------------------------------------------------------------------------
--- Library for representation of positions in first-order terms.
---
--- @author Jan-Hendrik Matthes
--- @version May 2016
--- @category algorithm
------------------------------------------------------------------------------
module Rewriting.Position
( Pos
, eps, showPos, isPosAbove, isPosBelow, isPosLeft, isPosRight
, isPosDisjunct, positions, (|>), replaceTerm
) where
import List (intercalate, isPrefixOf)
import Rewriting.Term (Term (..))
-- ---------------------------------------------------------------------------
-- Representation of positions in first-order terms
-- ---------------------------------------------------------------------------
--- A position in a term represented as a list of integers greater than zero.
type Pos = [Int]
--- The root position of a term.
eps :: Pos
eps = []
-- ---------------------------------------------------------------------------
-- Pretty-printing of positions in first-order terms
-- ---------------------------------------------------------------------------
-- \x00b7 = MIDDLE DOT
-- \x03b5 = GREEK SMALL LETTER EPSILON
--- Transforms a position into a string representation.
showPos :: Pos -> String
showPos [] = "\x03b5"
showPos ps@(_:_) = intercalate "\x00b7" (map show ps)
-- ---------------------------------------------------------------------------
-- Functions for positions in first-order terms
-- ---------------------------------------------------------------------------
--- Checks whether the first position is above the second position.
isPosAbove :: Pos -> Pos -> Bool
isPosAbove = isPrefixOf
--- Checks whether the first position is below the second position.
isPosBelow :: Pos -> Pos -> Bool
isPosBelow = flip isPrefixOf
--- Checks whether the first position is left from the second position.
isPosLeft :: Pos -> Pos -> Bool
isPosLeft [] _ = False
isPosLeft (_:_) [] = False
isPosLeft (p:ps) (q:qs) = case compare p q of
LT -> True
EQ -> isPosLeft ps qs
GT -> False
--- Checks whether the first position is right from the second position.
isPosRight :: Pos -> Pos -> Bool
isPosRight [] _ = False
isPosRight (_:_) [] = False
isPosRight (p:ps) (q:qs) = case compare p q of
LT -> False
EQ -> isPosRight ps qs
GT -> True
--- Checks whether the first position is disjunct from the second position.
isPosDisjunct :: Pos -> Pos -> Bool
isPosDisjunct p q = not (isPosAbove p q || isPosAbove q p)
--- Returns a list of all positions in a term.
positions :: Term _ -> [Pos]
positions (TermVar _) = [eps]
positions (TermCons _ ts) = eps:[i:p | (i, t) <- zip [1..] ts,
p <- positions t]
-- ---------------------------------------------------------------------------
-- Subterms and term replacement
-- ---------------------------------------------------------------------------
--- Selects the subterm at the given position.
(|>) :: Term f -> Pos -> Term f
t |> [] = t
(TermCons _ ts) |> (i:p) | i > 0 && i <= length ts = (ts !! (i - 1)) |> p
--- Replaces the subterm at the given position with the given term.
---
--- @param term - The term with the subterm to replace.
--- @param pos - The position of the subterm.
--- @param rterm - The new subterm.
--- @return The term with the new subterm.
replaceTerm :: Term f -> Pos -> Term f -> Term f
replaceTerm _ [] s = s
replaceTerm (TermCons c ts) (i:p) s
| i > 0 && i <= length ts = let (ts1, ti:ts2) = splitAt (i - 1) ts
in TermCons c (ts1 ++ (replaceTerm ti p s):ts2)
\ No newline at end of file
------------------------------------------------------------------------------
--- Library for representation of rules and term rewriting systems.
---
--- @author Jan-Hendrik Matthes
--- @version May 2016
--- @category algorithm
------------------------------------------------------------------------------
module Rewriting.Rules
( Rule, TRS
, showRule, showTRS, rRoot, rCons, rVars, normalise, isVariantOf
, renameRVars
) where
import Function (on)
import List (nub)
import Rewriting.Substitution (emptySubst, extendSubst, applySubst)
import Rewriting.Term
-- ---------------------------------------------------------------------------
-- Representation of rules and term rewriting systems
-- ---------------------------------------------------------------------------
--- A rule represented as a pair of terms and parameterized over the kind of
--- function symbols, e.g., strings.
type Rule f = (Term f, Term f)
--- A term rewriting system represented as a list of rules and parameterized
--- over the kind of function symbols, e.g., strings.
type TRS f = [Rule f]
-- ---------------------------------------------------------------------------
-- Pretty-printing of rules and term rewriting systems
-- ---------------------------------------------------------------------------
-- \x2192 = RIGHTWARDS ARROW
--- Transforms a rule into a string representation.
showRule :: (f -> String) -> Rule f -> String
showRule s (l, r) = (showTerm s l) ++ " \x2192 " ++ (showTerm s r)
--- Transforms a term rewriting system into a string representation.
showTRS :: (f -> String) -> TRS f -> String
showTRS s trs = unlines (map (showRule s) trs)
-- ---------------------------------------------------------------------------
-- Functions for rules and term rewriting systems
-- ---------------------------------------------------------------------------
--- Returns the root symbol (variable or constructor) of a rule.
rRoot :: Rule f -> Either VarIdx f
rRoot (l, _) = tRoot l
--- Returns all constructors in a rule.
rCons :: Rule f -> [f]
rCons (l, r) = nub (tCons l ++ tCons r)
--- Returns all variables in a rule.
rVars :: Rule _ -> [VarIdx]
rVars (l, _) = tVars l
--- Normalises a rule by renaming all variables in increasing order.
normalise :: Rule f -> Rule f
normalise rule@(l, r) = (applySubst sub l, applySubst sub r)
where
vMap = zip (rVars rule) (map TermVar [0..])
sub = foldr (\(v, t) subst -> extendSubst subst v t) emptySubst vMap
--- Checks whether the first rule is a variant of the second rule.
isVariantOf :: Rule f -> Rule f -> Bool
isVariantOf = on (==) normalise
--- Increases the variables in a rule by the given number.
renameRVars :: Int -> Rule f -> Rule f
renameRVars i (l, r) = (renameTVars i l, renameTVars i r)
\ No newline at end of file
------------------------------------------------------------------------------
--- Library for representation of substitutions on first-order terms.
---
--- @author Michael Hanus, Jonas Oberschweiber, Bjoern Peemoeller
--- @version November 2015
--- @category algorithm
------------------------------------------------------------------------------
module Rewriting.Substitution
( Subst
, showSubst, emptySubst, extendSubst, lookupSubst, applySubst
) where
import FiniteMap
import Rewriting.Term
-- ---------------------------------------------------------------------------
-- Substitution on terms
-- ---------------------------------------------------------------------------
--- The (abstract) data type for substitutions.
type Subst f = FM VarIdx (Term f)
--- Pretty string representation of a substitution.
showSubst :: Subst _ -> String
showSubst = unlines . map showOne . fmToList
where showOne (k, v) = show k ++ " -> " ++ show v
--- The empty substitution
emptySubst :: Subst _
emptySubst = emptyFM (<)
--- Extend the substitution with the given mapping.
---
--- @param subst - the substitution
--- @param index - the variable which should be mapped
--- @param term - the term the variable should be mapped to
--- @return the extended substitution
extendSubst :: Subst f -> VarIdx -> Term f-> Subst f
extendSubst = addToFM
--- Searches the substitution for a mapping from the given variable index
--- to a term.
---
--- @param subst - the substitution to search
--- @param i - the index to search for
--- @return the found term or Nothing
lookupSubst :: Subst f -> VarIdx -> Maybe (Term f)
lookupSubst = lookupFM
--- Applies a substitution to a single term.
---
--- @param sub - the substitution to apply
--- @param t - the term to apply the substitution to
--- @return the resulting term
applySubst :: Subst f -> Term f -> Term f
applySubst s t@(TermVar n) = maybe t id (lookupSubst s n)
applySubst s (TermCons c vs) = TermCons c (map (applySubst s) vs)
--- Applies a substitution to a single equation.
---
--- @param sub - the substitution to apply
--- @param eq - the equation to apply the substitution to
--- @return the resulting equation
substituteSingle :: Subst f -> TermEq f -> TermEq f
substituteSingle s (a, b) = (applySubst s a, applySubst s b)
--- Applies a substitution to a list of equations.
---
--- @param sub - the substitution to apply
--- @param eqs - the equations to apply the substitution to
--- @return the resulting equations
substitute :: Subst f -> TermEqs f -> TermEqs f
substitute s eqs = map (substituteSingle s) eqs
------------------------------------------------------------------------------
--- Library for representation of first-order terms.
---
--- This library is the basis of other libraries for the manipulation of
--- first-order terms, e.g., unification of terms. Therefore, this library
--- also defines other structures, like term equations.
---
--- @author Jan-Hendrik Matthes
--- @version May 2016
--- @category algorithm
------------------------------------------------------------------------------
module Rewriting.Term
( VarIdx, Term (..), TermEq, TermEqs
, showVarIdx, showTerm, showTermEq, showTermEqs, tConst, tRoot, tCons, tVars
, tVarsL, isConsTerm, isVarTerm, isGround, isLinear, mapTerm, renameTVars
) where
import List (intercalate, nub)
-- ---------------------------------------------------------------------------
-- Representation of first-order terms and term equations
-- ---------------------------------------------------------------------------
--- A variable represented as an integer greater than or equal to zero.
type VarIdx = Int
--- Representation of a first-order term, parameterized over the kind of
--- function symbols, e.g., strings.
---
--- @cons TermVar v - The variable with index `v`.
--- @cons TermCons c ts - The constructor with constructor `c` and argument
--- terms `ts`.
data Term f = TermVar VarIdx | TermCons f [Term f]
--- A term equation represented as a pair of terms and parameterized over the
--- kind of function symbols, e.g., strings.
type TermEq f = (Term f, Term f)
--- Multiple term equations represented as a list of term equations and
--- parameterized over the kind of function symbols, e.g., strings.
type TermEqs f = [TermEq f]
-- ---------------------------------------------------------------------------
-- Pretty-printing of first-order terms and term equations
-- ---------------------------------------------------------------------------
--- Transforms a variable into a string representation.
showVarIdx :: VarIdx -> String
showVarIdx v | v >= 0 = if q == 0
then [c]
else c:(show q)
where
(q, r) = divMod v 26
c = "abcdefghijklmnopqrstuvwxyz" !! r
--- Transforms a term into a string representation.
showTerm :: (f -> String) -> Term f -> String
showTerm _ (TermVar v) = showVarIdx v
showTerm s (TermCons c ts) = case ts of
[] -> s c
(_:_) -> (s c) ++ "(" ++ args ++ ")"
where
args = intercalate ", " (map (showTerm s) ts)
--- Transforms a term equation into a string representation.
showTermEq :: (f -> String) -> TermEq f -> String
showTermEq s (l, r) = (showTerm s l) ++ " = " ++ (showTerm s r)
--- Transforms multiple term equations into a string representation.
showTermEqs :: (f -> String) -> TermEqs f -> String
showTermEqs s eqs = unlines (map (showTermEq s) eqs)
-- ---------------------------------------------------------------------------
-- Functions for first-order terms
-- ---------------------------------------------------------------------------
--- Returns a term with the given constructor and no argument terms.
tConst :: f -> Term f
tConst c = TermCons c []
--- Returns the root symbol (variable or constructor) of a term.
tRoot :: Term f -> Either VarIdx f
tRoot (TermVar v) = Left v
tRoot (TermCons c _) = Right c
--- Returns all constructors in a term.
tCons :: Term f -> [f]
tCons (TermVar _) = []
tCons (TermCons c ts) = nub (c:(concatMap tCons ts))
--- Returns all variables in a term.
tVars :: Term _ -> [VarIdx]
tVars = nub . tVarsL
--- Returns a list of all variables in a term.
tVarsL :: Term _ -> [VarIdx]
tVarsL (TermVar v) = [v]
tVarsL (TermCons _ ts) = concatMap tVarsL ts
--- Checks whether a term is a constructor.
isConsTerm :: Term _ -> Bool
isConsTerm (TermVar _) = False
isConsTerm (TermCons _ _) = True
--- Checks whether a term is a variable.
isVarTerm :: Term _ -> Bool
isVarTerm (TermVar _) = True
isVarTerm (TermCons _ _) = False
--- Checks whether a term is a ground term (contains no variables).
isGround :: Term _ -> Bool
isGround = null . tVars
--- Checks whether a term is linear (contains no variable more than once).
isLinear :: Term _ -> Bool
isLinear = unique . tVarsL
--- Transforms a term by applying a transformation on all function symbols.
mapTerm :: (a -> b) -> Term a -> Term b
mapTerm _ (TermVar v) = TermVar v
mapTerm f (TermCons c ts) = TermCons (f c) (map (mapTerm f) ts)
--- Increases the variables in a term by the given number.
renameTVars :: Int -> Term f -> Term f
renameTVars i (TermVar v) = TermVar (v + i)
renameTVars i (TermCons c ts) = TermCons c (map (renameTVars i) ts)
-- ---------------------------------------------------------------------------
-- Definition of helper functions
-- ---------------------------------------------------------------------------
--- Checks whether a list contains no element more than once.
unique :: [_] -> Bool
unique [] = True
unique (x:xs) | notElem x xs = unique xs