...
 
Commits (6)
{
"name": "rewriting",
"version": "0.0.1",
"version": "2.0.0",
"author": "Jan-Hendrik Matthes, Michael Hanus <mh@informatik.uni-kiel.de>",
"maintainer": "Michael Hanus <mh@informatik.uni-kiel.de>",
"synopsis": "Libraries for term rewriting and narrowing",
......@@ -14,11 +14,11 @@
PAKCS/KiCS2 distributions.",
"category": [ "Rewriting", "Narrowing" ],
"dependencies": {
"abstract-curry" : ">= 1.0.0"
"abstract-curry": ">= 2.0.0"
},
"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",
......
......@@ -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
......@@ -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
......
......@@ -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
......
......@@ -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))) ++ "\"];"
......
......@@ -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
......
......@@ -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
......@@ -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)
-- ---------------------------------------------------------------------------
......
......@@ -37,6 +37,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.
......@@ -102,7 +103,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
......@@ -182,7 +183,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) =
......@@ -197,7 +198,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
......@@ -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
......@@ -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
-> Either (UnificationError f) (TermEqs f)
unify' sub [] = Right sub
unify' sub ((TermVar v, r@(TermCons _ _)):eqs) = elim sub v r eqs
unify' sub ((l@(TermCons _ _), TermVar v):eqs) = elim sub v l eqs
......@@ -87,7 +87,7 @@ unify' sub ((l@(TermCons c1 ts1), r@(TermCons c2 ts2)):eqs)
--- Substitutes a variable by a term inside a substitution and a list of term
--- equations that have yet to be unified. Also adds a mapping from that
--- variable to that term to the substitution.
elim :: TermEqs f -> VarIdx -> Term f -> TermEqs f
elim :: Eq f => TermEqs f -> VarIdx -> Term f -> TermEqs f
-> Either (UnificationError f) (TermEqs f)
elim sub v t eqs | dependsOn (TermVar v) t = Left (OccurCheck v t)
| otherwise = unify' sub' (substitute v t eqs)
......@@ -113,9 +113,8 @@ substituteSingle :: VarIdx -> Term f -> TermEq f -> TermEq f
substituteSingle v t = both (termSubstitute v t)
--- Checks whether the first term occurs as a subterm of the second term.
dependsOn :: Term f -> Term f -> Bool
dependsOn :: Eq f => Term f -> Term f -> Bool
dependsOn l r = and [not (l == r), dependsOn' l r]
where
dependsOn' :: Term f -> Term f -> Bool
dependsOn' t v@(TermVar _) = t == v
dependsOn' t (TermCons _ ts) = any id (map (dependsOn' t) ts)
\ No newline at end of file