Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
curry-packages
rewriting
Commits
d16eb800
Commit
d16eb800
authored
May 08, 2017
by
Michael Hanus
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Typeclass version packaged
parent
a298d48a
Changes
11
Hide whitespace changes
Inline
Side-by-side
Showing
11 changed files
with
82 additions
and
88 deletions
+82
-88
package.json
package.json
+3
-3
src/Rewriting/CriticalPairs.curry
src/Rewriting/CriticalPairs.curry
+3
-3
src/Rewriting/DefinitionalTree.curry
src/Rewriting/DefinitionalTree.curry
+15
-18
src/Rewriting/Files.curry
src/Rewriting/Files.curry
+2
-2
src/Rewriting/Narrowing.curry
src/Rewriting/Narrowing.curry
+18
-19
src/Rewriting/Rules.curry
src/Rewriting/Rules.curry
+5
-6
src/Rewriting/Strategy.curry
src/Rewriting/Strategy.curry
+19
-19
src/Rewriting/Substitution.curry
src/Rewriting/Substitution.curry
+0
-1
src/Rewriting/Term.curry
src/Rewriting/Term.curry
+5
-4
src/Rewriting/Unification.curry
src/Rewriting/Unification.curry
+6
-6
src/Rewriting/UnificationSpec.curry
src/Rewriting/UnificationSpec.curry
+6
-7
No files found.
package.json
View file @
d16eb800
{
"name"
:
"rewriting"
,
"version"
:
"0.0
.1
"
,
"version"
:
"
2.
0.0"
,
"author"
:
"Jan-Hendrick Matthes, Michael Hanus <mh@informatik.uni-kiel.de>"
,
"maintainer"
:
"Michael Hanus <mh@informatik.uni-kiel.de>"
,
"synopsis"
:
"Libraries for term rewriting and narrowing"
,
...
...
@@ -15,8 +15,8 @@
"category"
:
[
"Rewriting"
,
"Narrowing"
],
"dependencies"
:
{
},
"compilerCompatibility"
:
{
"pakcs"
:
">=
1.14.0, <
2.0.0"
,
"kics2"
:
">=
0.5.0, <
2.0.0"
"pakcs"
:
">= 2.0.0"
,
"kics2"
:
">= 2.0.0"
},
"exportedModules"
:
[
"Rewriting.CriticalPairs"
,
"Rewriting.Narrowing"
,
"Rewriting.Strategy"
,
...
...
src/Rewriting/CriticalPairs.curry
View file @
d16eb800
...
...
@@ -47,7 +47,7 @@ showCPairs s = unlines . (map (showCPair s))
-- ---------------------------------------------------------------------------
--- Returns the critical pairs of a term rewriting system.
cPairs :: TRS f -> [CPair f]
cPairs ::
Eq f =>
TRS f -> [CPair f]
cPairs trs
= let trs' = maybe trs (\v -> renameTRSVars (v + 1) trs) (maxVarInTRS trs)
in nub [(applySubst sub r1,
...
...
@@ -63,9 +63,9 @@ cPairs trs
-- ---------------------------------------------------------------------------
--- Checks whether a term rewriting system is orthogonal.
isOrthogonal :: TRS
_
-> Bool
isOrthogonal ::
Eq f =>
TRS
f
-> Bool
isOrthogonal trs = (isLeftLinear trs) && (null (cPairs trs))
--- Checks whether a term rewriting system is weak-orthogonal.
isWeakOrthogonal :: TRS
_
-> Bool
isWeakOrthogonal ::
Eq f =>
TRS
f
-> Bool
isWeakOrthogonal trs = (isLeftLinear trs) && (all (uncurry (==)) (cPairs trs))
\ No newline at end of file
src/Rewriting/DefinitionalTree.curry
View file @
d16eb800
...
...
@@ -58,12 +58,12 @@ dtPattern (Or pat _) = pat
--- Checks whether a term has a definitional tree with the same constructor
--- pattern in the given list of definitional trees.
hasDefTree :: [DefTree f] -> Term f -> Bool
hasDefTree ::
Eq f =>
[DefTree f] -> Term f -> Bool
hasDefTree dts t = any ((eqConsPattern t) . dtPattern) dts
--- Returns a list of definitional trees with the same constructor pattern for
--- a term from the given list of definitional trees.
selectDefTrees :: [DefTree f] -> Term f -> [DefTree f]
selectDefTrees ::
Eq f =>
[DefTree f] -> Term f -> [DefTree f]
selectDefTrees dts t = filter ((eqConsPattern t) . dtPattern) dts
--- Returns the definitional tree with the given index from the given list of
...
...
@@ -84,19 +84,18 @@ idtPositions trs@((l, _):_)
all (isDemandedAt i) trs]
--- Returns a list of definitional trees for a term rewriting system.
defTrees :: TRS f -> [DefTree f]
defTrees ::
Eq f =>
TRS f -> [DefTree f]
defTrees = (concatMap defTreesS) . (groupBy eqCons) . (sortBy eqCons)
where
eqCons :: Rule f -> Rule f -> Bool
eqCons = on eqConsPattern fst
--- Returns a list of definitional trees for a list of term rewriting systems.
defTreesL :: [TRS f] -> [DefTree f]
defTreesL ::
Eq f =>
[TRS f] -> [DefTree f]
defTreesL = defTrees . concat
--- Returns a list of definitional trees for a term rewriting system, whose
--- rules have the same constructor pattern.
defTreesS :: TRS f -> [DefTree f]
defTreesS ::
Eq f =>
TRS f -> [DefTree f]
defTreesS [] = []
defTreesS trs@((l, _):_)
= case l of
...
...
@@ -111,7 +110,7 @@ defTreesS trs@((l, _):_)
--- the same constructor pattern, with the given list of inductive positions,
--- the given pattern and the given next possible variable or `Nothing` if no
--- such definitional tree exists.
defTreesS' :: VarIdx -> TRS f -> [Pos] -> Term f -> Maybe (DefTree f)
defTreesS' ::
Eq f =>
VarIdx -> TRS f -> [Pos] -> Term f -> Maybe (DefTree f)
defTreesS' _ [] [] _ = Nothing
defTreesS' v [r] [] pat = mkLeaf v pat r
defTreesS' v trs@(_:_:_) [] pat
...
...
@@ -124,14 +123,14 @@ defTreesS' v trs (p:ps) pat = Just (Branch pat p dts)
dts = catMaybes [defTreesS' v' (selectRules v' pat') ps pat' |
pat' <- pats,
let v' = max v (maybe 0 (+ 1) (maxVarInTerm pat'))]
selectRules :: VarIdx -> Term f -> TRS f
selectRules v' t = [r | r@(l, _) <- renameTRSVars v' trs,
unifiable [(l, t)]]
--- Returns a definitional tree for the given pattern, the given rule and the
--- given next possible variable or `Nothing` if no such definitional tree
--- exists.
mkLeaf :: VarIdx -> Term f -> Rule f -> Maybe (DefTree f)
mkLeaf ::
Eq f =>
VarIdx -> Term f -> Rule f -> Maybe (DefTree f)
mkLeaf v pat r
= case unify [(l, pat)] of
(Left _) -> Nothing
...
...
@@ -149,7 +148,7 @@ mkLeaf v pat r
--- rewriting systems and the given next possible variable or `Nothing` if no
--- such definitional tree exists. Only the rules in the first term rewriting
--- system of the pair have a demanded first argument position.
mkOr :: VarIdx -> Term f -> (TRS f, TRS f) -> Maybe (DefTree f)
mkOr ::
Eq f =>
VarIdx -> Term f -> (TRS f, TRS f) -> Maybe (DefTree f)
mkOr _ _ ([], []) = Nothing
mkOr v pat ([], rs2@(_:_)) = let mdts = map (mkLeaf v pat) rs2
in Just (Or pat (catMaybes mdts))
...
...
@@ -174,11 +173,10 @@ varPositions (TermCons _ ts) = [[i] | i <- [1..(length ts)],
--- Returns the position and the definitional trees from the given list of
--- definitional trees for the leftmost outermost defined constructor in a
--- term or `Nothing` if no such pair exists.
loDefTrees :: [DefTree f] -> Term f -> Maybe (Pos, [DefTree f])
loDefTrees ::
Eq f =>
[DefTree f] -> Term f -> Maybe (Pos, [DefTree f])
loDefTrees [] _ = Nothing
loDefTrees dts@(_:_) t = listToMaybe (loDefTrees' eps t)
where
loDefTrees' :: Pos -> Term f -> [(Pos, [DefTree f])]
loDefTrees' _ (TermVar _) = []
loDefTrees' p c@(TermCons _ ts)
| hasDefTree dts c = [(p, selectDefTrees dts c)]
...
...
@@ -187,7 +185,7 @@ loDefTrees dts@(_:_) t = listToMaybe (loDefTrees' eps t)
--- The reduction strategy phi. It uses the definitional tree with the given
--- index for all constructor terms if possible or at least the first one.
phiRStrategy :: Int -> RStrategy
_
phiRStrategy ::
Eq f =>
Int -> RStrategy
f
phiRStrategy n trs t
= let dts = defTrees trs
in case loDefTrees dts t of
...
...
@@ -202,7 +200,7 @@ phiRStrategy n trs t
--- reduced according to the given definitional tree or `Nothing` if no such
--- position exists. It uses the definitional tree with the given index for
--- all constructor terms if possible or at least the first one.
phiRStrategy' :: Int -> [DefTree f] -> Term f -> DefTree f -> Maybe Pos
phiRStrategy' ::
Eq f =>
Int -> [DefTree f] -> Term f -> DefTree f -> Maybe Pos
phiRStrategy' _ _ t (Leaf (l, _))
| unifiable [(l', t)] = Just eps
| otherwise = Nothing
...
...
@@ -276,7 +274,6 @@ toGraph dt = fst (fst (runState (toGraph' dt) 0))
showTermWithPos :: (f -> String) -> (Maybe Pos, Term f) -> String
showTermWithPos s = showTP False
where
showTerm' :: Bool -> Term f -> String
showTerm' _ (TermVar v) = showVarIdx v
showTerm' b (TermCons c ts)
= case ts of
...
...
@@ -285,7 +282,7 @@ showTermWithPos s = showTP False
++ (showTerm' True r))
_ -> (s c) ++ "("
++ (intercalate "," (map (showTerm' False) ts)) ++ ")"
showTP :: Bool -> (Maybe Pos, Term f) -> String
showTP b (Nothing, t) = showTerm' b t
showTP b (Just [], t) = "<u>" ++ (showTerm' b t) ++ "</u>"
showTP _ (Just (_:_), TermVar v) = showVarIdx v
...
...
@@ -308,10 +305,10 @@ dotifyDefTree s dt = "digraph DefinitionalTree {\n\t"
++ (unlines (map showEdge es)) ++ "}"
where
(ns, es) = toGraph dt
showNode :: Node _ -> String
showNode (n, p, t) = "\t" ++ (showVarIdx n) ++ " [label=<"
++ (showTermWithPos s (p, t)) ++ ">];"
showEdge :: Edge _ -> String
showEdge (b, (n1, _, _), (n2, _, _))
= let opts = if b then " [arrowhead=normal];" else ";"
in "\t" ++ (showVarIdx n1) ++ " -> " ++ (showVarIdx n2) ++ opts
...
...
src/Rewriting/Files.curry
View file @
d16eb800
...
...
@@ -4,7 +4,7 @@
--- rewriting system and every type has a corresponding type declaration.
---
--- @author Jan-Hendrik Matthes
--- @version
August
2016
--- @version
October
2016
--- @category algorithm
------------------------------------------------------------------------------
...
...
@@ -79,7 +79,7 @@ readCurryProgram fn = do res <- tryReadCurryFile fn
--- where every function gets assigned the corresponding term rewriting system
--- and every type has a corresponding type declaration.
fromCurryProg :: CurryProg -> RWData
fromCurryProg (CurryProg _ _ ts fs _)
fromCurryProg (CurryProg _ _
_ _ _
ts fs _)
= (listToFM (<) (map fromFuncDecl fs), ts)
--- Transforms an abstract curry function declaration into a pair with
...
...
src/Rewriting/Narrowing.curry
View file @
d16eb800
...
...
@@ -73,7 +73,7 @@ data NarrowingTree f = NTree (Term f) [(Pos, Subst f, NarrowingTree f)]
data NOptions f = NOptions { normalize :: Bool, rStrategy :: RStrategy f }
--- The default narrowing options.
defaultNOptions :: NOptions
_
defaultNOptions ::
Eq f =>
NOptions
f
defaultNOptions = NOptions { normalize = False, rStrategy = poRStrategy }
-- ---------------------------------------------------------------------------
...
...
@@ -95,28 +95,28 @@ showNarrowing s (NStep t p sub n)
-- ---------------------------------------------------------------------------
--- The standard narrowing strategy.
stdNStrategy :: NStrategy
_
stdNStrategy ::
Eq f =>
NStrategy
f
stdNStrategy trs t = [(p, rule, sub) |
p <- positions t, let tp = t |> p, isConsTerm tp,
rule@(l, _) <- trs,
(Right sub) <- [unify [(tp, l)]]]
--- The innermost narrowing strategy.
imNStrategy :: NStrategy
_
imNStrategy ::
Eq f =>
NStrategy
f
imNStrategy trs t = [(p, rule, sub) |
p <- positions t, let tp = t |> p, isPattern trs tp,
rule@(l, _) <- trs,
(Right sub) <- [unify [(tp, l)]]]
--- The outermost narrowing strategy.
omNStrategy :: NStrategy
_
omNStrategy ::
Eq f =>
NStrategy
f
omNStrategy trs t = let ns = stdNStrategy trs t
in [n | n@(p, _, _) <- ns,
all (\p' -> not (above p' p))
[p' | (p', _, _) <- ns, p' /= p]]
--- The leftmost outermost narrowing strategy.
loNStrategy :: NStrategy
_
loNStrategy ::
Eq f =>
NStrategy
f
loNStrategy trs t
= let ns = stdNStrategy trs t
in [n | n@(p, _, _) <- ns,
...
...
@@ -124,14 +124,14 @@ loNStrategy trs t
[p' | (p', _, _) <- ns, p' /= p]]
--- The lazy narrowing strategy.
lazyNStrategy :: NStrategy
_
lazyNStrategy ::
Eq f =>
NStrategy
f
lazyNStrategy trs t
= let lps = lazyPositions trs t
in filter (\(p, _, _) -> elem p lps) (stdNStrategy trs t)
--- Returns a list of all lazy positions in a term according to the given term
--- rewriting system.
lazyPositions :: TRS f -> Term f -> [Pos]
lazyPositions ::
Eq f =>
TRS f -> Term f -> [Pos]
lazyPositions _ (TermVar _) = []
lazyPositions trs t@(TermCons _ ts)
| isRedex trs t = if null rs then lps else eps:lps
...
...
@@ -143,7 +143,7 @@ lazyPositions trs t@(TermCons _ ts)
lps = [i:p | i <- dps, p <- lazyPositions trs (ts !! (i - 1))]
--- The weakly needed narrowing strategy.
wnNStrategy :: NStrategy
_
wnNStrategy ::
Eq f =>
NStrategy
f
wnNStrategy trs t
= let dts = defTrees trs
v = fromMaybe 0 (minVarInTRS trs)
...
...
@@ -156,7 +156,7 @@ wnNStrategy trs t
--- Returns the narrowing steps for the weakly needed narrowing strategy
--- according to the given definitional tree and the given next possible
--- variable.
wnNStrategy' :: [DefTree f] -> VarIdx -> Term f -> DefTree f
wnNStrategy' ::
Eq f =>
[DefTree f] -> VarIdx -> Term f -> DefTree f
-> [(Pos, Rule f, Subst f)]
wnNStrategy' _ v t (Leaf r)
= let rule@(l, _) = renameRuleVars v (normalizeRule r)
...
...
@@ -173,7 +173,6 @@ wnNStrategy' dts v t (Branch pat p dts')
in [(p .> p', rule, composeSubst sub tau') |
(p', rule, sub) <- wnNStrategy' dts v' (t' |> p) dt]
where
filterDTS :: [DefTree f] -> [DefTree f]
filterDTS = filter (\dt -> let dtp = renameTermVars v (dtPattern dt)
in unifiable [(t, dtp)])
wnNStrategy' dts v t (Or _ dts') = concatMap (wnNStrategy' dts v t) dts'
...
...
@@ -205,7 +204,6 @@ narrowBy' v sub s trs n t
[] -> [(sub, t)]
ns@(_:_) -> concatMap combine ns
where
combine :: (Pos, Rule f, Subst f) -> [(Subst f, Term f)]
combine (p, (_, r), sub')
= let t' = applySubst sub' (replaceTerm t p r)
rsub' = restrictSubst sub' (tVars t)
...
...
@@ -237,7 +235,7 @@ narrowingBy' v sub s trs n t
[] -> [NTerm t]
ns@(_:_) -> concatMap combine ns
where
combine :: (Pos, Rule f, Subst f) -> [Narrowing f]
--
combine :: (Pos, Rule f, Subst f) -> [Narrowing f]
combine (p, (_, r), sub')
= let t' = applySubst sub' (replaceTerm t p r)
rsub' = restrictSubst sub' (tVars t)
...
...
@@ -271,7 +269,7 @@ narrowingTreeBy' v sub s trs n t
| otherwise = NTree t (map combine (s trs' t))
where
trs' = renameTRSVars v (normalizeTRS trs)
combine :: (Pos, Rule f, Subst f) -> (Pos, Subst f, NarrowingTree f)
--
combine :: (Pos, Rule f, Subst f) -> (Pos, Subst f, NarrowingTree f)
combine (p, (_, r), sub')
= let t' = applySubst sub' (replaceTerm t p r)
rsub' = restrictSubst sub' (tVars t)
...
...
@@ -286,7 +284,7 @@ narrowingTreeBy' v sub s trs n t
--- `TermCons c [l, r]` with `c` being a constructor like `=`. The term `l`
--- and the term `r` are the left-hand side and the right-hand side of the
--- term equation.
solveEq :: NOptions f -> NStrategy f -> TRS f -> Term f -> [Subst f]
solveEq ::
Eq f =>
NOptions f -> NStrategy f -> TRS f -> Term f -> [Subst f]
solveEq _ _ _ (TermVar _) = []
solveEq opts s trs t@(TermCons _ ts)
= case ts of
...
...
@@ -301,7 +299,7 @@ solveEq opts s trs t@(TermCons _ ts)
--- `TermCons c [l, r]` with `c` being a constructor like `=`. The term `l`
--- and the term `r` are the left-hand side and the right-hand side of the
--- term equation.
solveEqL :: NOptions f -> NStrategy f -> [TRS f] -> Term f -> [Subst f]
solveEqL ::
Eq f =>
NOptions f -> NStrategy f -> [TRS f] -> Term f -> [Subst f]
solveEqL opts s trss = solveEq opts s (concat trss)
--- Solves a term equation with the given strategy, the given term rewriting
...
...
@@ -310,7 +308,8 @@ solveEqL opts s trss = solveEq opts s (concat trss)
--- `TermCons c [l, r]` with `c` being a constructor like `=`. The term `l`
--- and the term `r` are the left-hand side and the right-hand side of the
--- term equation.
solveEq' :: NOptions f -> VarIdx -> Subst f -> NStrategy f -> TRS f -> Term f
solveEq' :: Eq f =>
NOptions f -> VarIdx -> Subst f -> NStrategy f -> TRS f -> Term f
-> [Subst f]
solveEq' _ _ _ _ _ (TermVar _) = []
solveEq' opts v sub s trs t@(TermCons _ ts)
...
...
@@ -327,7 +326,7 @@ solveEq' opts v sub s trs t@(TermCons _ ts)
nt@(TermCons _ [l, r]) = if (normalize opts)
then reduce (rStrategy opts) trs t
else t
solve :: (Pos, Rule f, Subst f) -> [Subst f]
--
solve :: (Pos, Rule f, Subst f) -> [Subst f]
solve (p, (_, r'), sub')
= let t' = applySubst sub' (replaceTerm nt p r')
rsub' = restrictSubst sub' (tVars nt)
...
...
@@ -381,10 +380,10 @@ dotifyNarrowingTree s ng
++ (unlines (map showEdge es)) ++ "}"
where
(ns, es) = toGraph ng
showNode :: Node _ -> String
showNode (n, t) = "\t" ++ (showVarIdx n) ++ " [label=\"" ++ (showTerm s t)
++ "\"];"
showEdge :: Edge _ -> String
showEdge ((n1, t), sub, (n2, _))
= "\t" ++ (showVarIdx n1) ++ " -> " ++ (showVarIdx n2) ++ " [label=\""
++ (showSubst s (restrictSubst sub (tVars t))) ++ "\"];"
...
...
src/Rewriting/Rules.curry
View file @
d16eb800
...
...
@@ -55,7 +55,7 @@ rRoot :: Rule f -> Either VarIdx f
rRoot (l, _) = tRoot l
--- Returns a list without duplicates of all constructors in a rule.
rCons :: Rule f -> [f]
rCons ::
Eq f =>
Rule f -> [f]
rCons (l, r) = union (tCons l) (tCons r)
--- Returns a list without duplicates of all variables in a rule.
...
...
@@ -105,7 +105,7 @@ normalizeTRS :: TRS f -> TRS f
normalizeTRS = map normalizeRule
--- Checks whether the first rule is a variant of the second rule.
isVariantOf :: Rule f -> Rule f -> Bool
isVariantOf ::
Eq f =>
Rule f -> Rule f -> Bool
isVariantOf = on (==) normalizeRule
--- Checks whether a term rewriting system is left-linear.
...
...
@@ -118,22 +118,21 @@ isLeftNormal = all (isNormal . fst)
--- Checks whether a term is reducible with some rule
--- of the given term rewriting system.
isRedex :: TRS f -> Term f -> Bool
isRedex ::
Eq f =>
TRS f -> Term f -> Bool
isRedex trs t = any ((eqConsPattern t) . fst) trs
--- Checks whether a term is a pattern, i.e., an root-reducible term
--- where the argaccording to the given term rewriting
--- system.
isPattern :: TRS f -> Term f -> Bool
isPattern ::
Eq f =>
TRS f -> Term f -> Bool
isPattern _ (TermVar _) = False
isPattern trs t@(TermCons _ ts) = isRedex trs t && all isVarOrCons ts
where
isVarOrCons :: Term f -> Bool
isVarOrCons (TermVar _) = True
isVarOrCons t'@(TermCons _ ts') = not (isRedex trs t') && all isVarOrCons ts'
--- Checks whether a term rewriting system is constructor-based.
isConsBased :: TRS
_
-> Bool
isConsBased ::
Eq f =>
TRS
f
-> Bool
isConsBased trs = all ((isPattern trs) . fst) trs
--- Checks whether the given argument position of a rule is demanded. Returns
...
...
src/Rewriting/Strategy.curry
View file @
d16eb800
...
...
@@ -62,7 +62,7 @@ showReduction s (RStep t ps r) = (showTerm s t) ++ "\n\x2192" ++ "["
--- Returns the redex positions of a term according to the given term
--- rewriting system.
redexes :: TRS f -> Term f -> [Pos]
redexes ::
Eq f =>
TRS f -> Term f -> [Pos]
redexes trs t
= let trs' = maybe trs (\v -> renameTRSVars (v + 1) trs) (maxVarInTerm t)
in nub [p | p <- positions t, let tp = t |> p,
...
...
@@ -72,14 +72,14 @@ redexes trs t
--- Returns a sequential reduction strategy according to the given ordering
--- function.
seqRStrategy :: (Pos -> Pos -> Ordering) -> RStrategy
_
seqRStrategy ::
Eq f =>
(Pos -> Pos -> Ordering) -> RStrategy
f
seqRStrategy cmp trs t = case redexes trs t of
[] -> []
ps@(_:_) -> [minimumBy cmp ps]
--- Returns a parallel reduction strategy according to the given ordering
--- function.
parRStrategy :: (Pos -> Pos -> Ordering) -> RStrategy
_
parRStrategy ::
Eq f =>
(Pos -> Pos -> Ordering) -> RStrategy
f
parRStrategy cmp trs t = case redexes trs t of
[] -> []
ps@(_:_) -> head (groupBy g (sortBy s ps))
...
...
@@ -94,7 +94,7 @@ parRStrategy cmp trs t = case redexes trs t of
-- ---------------------------------------------------------------------------
--- The leftmost innermost reduction strategy.
liRStrategy :: RStrategy
_
liRStrategy ::
Eq f =>
RStrategy
f
liRStrategy = seqRStrategy liOrder
where
liOrder :: Pos -> Pos -> Ordering
...
...
@@ -104,7 +104,7 @@ liRStrategy = seqRStrategy liOrder
| otherwise = GT
--- The leftmost outermost reduction strategy.
loRStrategy :: RStrategy
_
loRStrategy ::
Eq f =>
RStrategy
f
loRStrategy = seqRStrategy loOrder
where
loOrder :: Pos -> Pos -> Ordering
...
...
@@ -114,7 +114,7 @@ loRStrategy = seqRStrategy loOrder
| otherwise = GT
--- The rightmost innermost reduction strategy.
riRStrategy :: RStrategy
_
riRStrategy ::
Eq f =>
RStrategy
f
riRStrategy = seqRStrategy riOrder
where
riOrder :: Pos -> Pos -> Ordering
...
...
@@ -124,7 +124,7 @@ riRStrategy = seqRStrategy riOrder
| otherwise = GT
--- The rightmost outermost reduction strategy.
roRStrategy :: RStrategy
_
roRStrategy ::
Eq f =>
RStrategy
f
roRStrategy = seqRStrategy roOrder
where
roOrder :: Pos -> Pos -> Ordering
...
...
@@ -134,7 +134,7 @@ roRStrategy = seqRStrategy roOrder
| otherwise = GT
--- The parallel innermost reduction strategy.
piRStrategy :: RStrategy
_
piRStrategy ::
Eq f =>
RStrategy
f
piRStrategy = parRStrategy piOrder
where
piOrder :: Pos -> Pos -> Ordering
...
...
@@ -144,7 +144,7 @@ piRStrategy = parRStrategy piOrder
| otherwise = EQ
--- The parallel outermost reduction strategy.
poRStrategy :: RStrategy
_
poRStrategy ::
Eq f =>
RStrategy
f
poRStrategy = parRStrategy poOrder
where
poOrder :: Pos -> Pos -> Ordering
...
...
@@ -158,18 +158,18 @@ poRStrategy = parRStrategy poOrder
-- ---------------------------------------------------------------------------
--- Reduces a term with the given strategy and term rewriting system.
reduce :: RStrategy f -> TRS f -> Term f -> Term f
reduce ::
Eq f =>
RStrategy f -> TRS f -> Term f -> Term f
reduce s trs t = case s trs t of
[] -> t
ps@(_:_) -> reduce s trs (reduceAtL trs ps t)
--- Reduces a term with the given strategy and list of term rewriting systems.
reduceL :: RStrategy f -> [TRS f] -> Term f -> Term f
reduceL ::
Eq f =>
RStrategy f -> [TRS f] -> Term f -> Term f
reduceL s trss = reduce s (concat trss)
--- Reduces a term with the given strategy and term rewriting system by the
--- given number of steps.
reduceBy :: RStrategy f -> TRS f -> Int -> Term f -> Term f
reduceBy ::
Eq f =>
RStrategy f -> TRS f -> Int -> Term f -> Term f
reduceBy s trs n t
| n <= 0 = t
| otherwise = case s trs t of
...
...
@@ -178,12 +178,12 @@ reduceBy s trs n t
--- Reduces a term with the given strategy and list of term rewriting systems
--- by the given number of steps.
reduceByL :: RStrategy f -> [TRS f] -> Int -> Term f -> Term f
reduceByL ::
Eq f =>
RStrategy f -> [TRS f] -> Int -> Term f -> Term f
reduceByL s trss = reduceBy s (concat trss)
--- Reduces a term with the given term rewriting system at the given redex
--- position.
reduceAt :: TRS f -> Pos -> Term f -> Term f
reduceAt ::
Eq f =>
TRS f -> Pos -> Term f -> Term f
reduceAt [] _ t = t
reduceAt (x:rs) p t
= case unify [(l, tp)] of
...
...
@@ -196,13 +196,13 @@ reduceAt (x:rs) p t
--- Reduces a term with the given term rewriting system at the given redex
--- positions.
reduceAtL :: TRS f -> [Pos] -> Term f -> Term f
reduceAtL ::
Eq f =>
TRS f -> [Pos] -> Term f -> Term f
reduceAtL _ [] t = t
reduceAtL trs (p:ps) t = reduceAtL trs ps (reduceAt trs p t)
--- Returns the reduction of a term with the given strategy and term rewriting
--- system.
reduction :: RStrategy f -> TRS f -> Term f -> Reduction f
reduction ::
Eq f =>
RStrategy f -> TRS f -> Term f -> Reduction f
reduction s trs t
= case s trs t of
[] -> NormalForm t
...
...
@@ -210,12 +210,12 @@ reduction s trs t
--- Returns the reduction of a term with the given strategy and list of term
--- rewriting systems.
reductionL :: RStrategy f -> [TRS f] -> Term f -> Reduction f
reductionL ::
Eq f =>
RStrategy f -> [TRS f] -> Term f -> Reduction f
reductionL s trss = reduction s (concat trss)
--- Returns the reduction of a term with the given strategy, the given term
--- rewriting system and the given number of steps.
reductionBy :: RStrategy f -> TRS f -> Int -> Term f -> Reduction f
reductionBy ::
Eq f =>
RStrategy f -> TRS f -> Int -> Term f -> Reduction f
reductionBy s trs n t
| n <= 0 = NormalForm t
| otherwise = case s trs t of
...
...
@@ -225,5 +225,5 @@ reductionBy s trs n t
--- Returns the reduction of a term with the given strategy, the given list of
--- term rewriting systems and the given number of steps.
reductionByL :: RStrategy f -> [TRS f] -> Int -> Term f -> Reduction f
reductionByL ::
Eq f =>
RStrategy f -> [TRS f] -> Int -> Term f -> Reduction f
reductionByL s trss = reductionBy s (concat trss)
\ No newline at end of file
src/Rewriting/Substitution.curry
View file @
d16eb800
...
...
@@ -37,7 +37,6 @@ showSubst :: (f -> String) -> Subst f -> String
showSubst s sub = "{" ++ (intercalate "," (map showMapping (fmToList sub)))
++ "}"
where
showMapping :: (VarIdx, Term f) -> String
showMapping (v, t) = (showVarIdx v) ++ " \x21a6 " ++ (showTerm s t)
-- ---------------------------------------------------------------------------
...
...
src/Rewriting/Term.curry
View file @
d16eb800
...
...
@@ -36,6 +36,7 @@ type VarIdx = Int
--- @cons TermCons c ts - The constructor term with constructor `c` and
--- argument terms `ts`.
data Term f = TermVar VarIdx | TermCons f [Term f]
deriving (Eq, Show)
--- A term equation represented as a pair of terms and parameterized over the
--- kind of function symbols, e.g., strings.
...
...
@@ -97,7 +98,7 @@ tRoot (TermVar v) = Left v
tRoot (TermCons c _) = Right c
--- Returns a list without duplicates of all constructors in a term.
tCons :: Term f -> [f]
tCons ::
Eq f =>
Term f -> [f]
tCons = nub . tConsAll
--- Returns a list of all constructors in a term. The resulting list may
...
...
@@ -177,7 +178,7 @@ mapTerm f (TermCons c ts) = TermCons (f c) (map (mapTerm f) ts)
--- Checks whether the constructor pattern of the first term is equal to the
--- constructor pattern of the second term. Returns `True` if both terms have
--- the same constructor and the same arity.
eqConsPattern :: Term f -> Term f -> Bool
eqConsPattern ::
Eq f =>
Term f -> Term f -> Bool
eqConsPattern (TermVar _) _ = False
eqConsPattern (TermCons _ _) (TermVar _) = False
eqConsPattern (TermCons c1 ts1) (TermCons c2 ts2) =
...
...
@@ -192,7 +193,7 @@ parensIf :: Bool -> String -> String
parensIf b s = if b then "(" ++ s ++ ")" else s
--- Checks whether a list contains no element more than once.
unique ::
[_
] -> Bool
unique ::
Eq a => [a
] -> Bool
unique [] = True
unique (x:xs) | notElem x xs = unique xs
| otherwise = False
\ No newline at end of file
| otherwise = False
src/Rewriting/Unification.curry
View file @
d16eb800
...
...
@@ -31,6 +31,7 @@ import Rewriting.UnificationSpec (UnificationError (..), showUnificationError)
--- an additional `Ref` constructor. This `Ref` constructor is used to
--- represent references into a reference table.
data RTerm f = Ref VarIdx | RTermVar VarIdx | RTermCons f [RTerm f]
deriving (Eq, Show)
--- A reference table used to store the values referenced by `Ref` terms
--- represented as a finite map from variables to `RTerm`s and parameterized
...
...
@@ -51,14 +52,14 @@ type REqs f = [REq f]
--- Unifies a list of term equations. Returns either a unification error or a
--- substitution.
unify :: TermEqs f -> Either (UnificationError f) (Subst f)
unify ::
Eq f =>
TermEqs f -> Either (UnificationError f) (Subst f)
unify eqs = let (rt, reqs) = termEqsToREqs eqs
in either Left
(\(rt', reqs') -> Right (eqsToSubst rt' reqs'))
(unify' rt [] reqs)
--- Checks whether a list of term equations can be unified.
unifiable :: TermEqs
_
-> Bool
unifiable ::
Eq f =>
TermEqs
f
-> Bool
unifiable = isRight . unify
-- ---------------------------------------------------------------------------
...
...
@@ -130,7 +131,7 @@ deref _ t@(RTermCons _ _) = t
-- ---------------------------------------------------------------------------
--- Internal unification function, the core of the algorithm.
unify' :: RefTable f -> REqs f -> REqs f
unify' ::
Eq f =>
RefTable f -> REqs f -> REqs f
-> Either (UnificationError f) (RefTable f, REqs f)
-- No equations left, we are done.
unify' rt sub [] = Right (rt, sub)
...
...
@@ -155,7 +156,7 @@ unify' rt sub (eq@(l, r):eqs)
--- yet to be unified and the right-hand sides of all equations of the result
--- list. Also adds a mapping from that variable to that term to the result
--- list.
elim :: RefTable f -> REqs f -> VarIdx -> RTerm f -> REqs f
elim ::
Eq f =>
RefTable f -> REqs f -> VarIdx -> RTerm f -> REqs f
-> Either (UnificationError f) (RefTable f, REqs f)
elim rt sub v t eqs
| dependsOn rt (RTermVar v) t = Left (OccurCheck v (rTermToTerm rt t))
...
...
@@ -169,10 +170,9 @@ elim rt sub v t eqs
(RTermCons _ _) -> unify' (addToFM rt v t) ((RTermVar v, t):sub) eqs
--- Checks whether the first term occurs as a subterm of the second term.
dependsOn :: RefTable f -> RTerm f -> RTerm f -> Bool
dependsOn ::
Eq f =>
RefTable f -> RTerm f -> RTerm f -> Bool
dependsOn rt l r = (l /= r) && (dependsOn' r)
where
dependsOn' :: RTerm f -> Bool
dependsOn' x@(Ref _) = (deref rt x) == l
dependsOn' t@(RTermVar _) = l == t
dependsOn' (RTermCons _ ts) = or (map dependsOn' ts)
\ No newline at end of file
src/Rewriting/UnificationSpec.curry
View file @
d16eb800
...
...
@@ -54,10 +54,9 @@ showUnificationError s (OccurCheck v t) = "OccurCheck: " ++ (showVarIdx v)
--- Unifies a list of term equations. Returns either a unification error or a
--- substitution.
unify :: TermEqs f -> Either (UnificationError f) (Subst f)
unify ::
(Eq f, Show f) =>
TermEqs f -> Either (UnificationError f) (Subst f)
unify = (either Left (Right . eqsToSubst)) . (unify' [])
where
eqsToSubst :: TermEqs f -> Subst f
eqsToSubst [] = emptySubst
eqsToSubst (eq@(l, r):eqs)
= case l of
...
...
@@ -68,13 +67,14 @@ unify = (either Left (Right . eqsToSubst)) . (unify' [])
(TermCons _ _) -> error ("eqsToSubst: " ++ (show eq))
--- Checks whether a list of term equations can be unified.
unifiable :: TermEqs
_
-> Bool
unifiable ::
(Eq f, Show f) =>
TermEqs
f
-> Bool
unifiable = isRight . unify
--- Unifies a list of term equations. The first argument specifies the current
--- substitution represented by term equations. Returns either a unification
--- error or a substitution represented by term equations.
unify' :: TermEqs f -> TermEqs f -> Either (UnificationError f) (TermEqs f)
unify' :: Eq f => TermEqs f -> TermEqs f