Commit 3954e816 authored by Michael Hanus's avatar Michael Hanus
Browse files

Code reformatting

parent ba29769c
## 2.1.0 (2020-02-13)
* Modernized the DOT output for definitional trees and narrowing graphs
* Added the `Rewriting.UnificationSpec` module to the list of exported modules
## 2.0.1 (2019-11-05)
* Fixed an infinite loop in the construction of definitional trees
## 2.0.0 (2019-10-16)
* First release
\ No newline at end of file
Copyright (c) 2016–2021, Jan-Hendrik Matthes
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
* Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
* 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.
* 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.
......@@ -5,24 +5,25 @@
"maintainer": "Michael Hanus <mh@informatik.uni-kiel.de>",
"synopsis": "Libraries for term rewriting and narrowing",
"description":
"These libraries provide a representation of first-order terms
"This package provides a representation of first-order terms
and various notions of term rewriting, like position, substitution,
unification, critical pairs, etc. Moreover, it defines also
operations for rewriting and narrowing strategies and a
representation of definitional trees.
A previous version of these libraries were part of the
A previous version of the contained libraries was part of the
PAKCS/KiCS2 distributions.",
"category": [ "Rewriting", "Narrowing" ],
"homepage": "https://github.com/matthesjh/rewriting-curry",
"repository": "https://github.com/matthesjh/rewriting-curry.git",
"bugReports": "https://github.com/matthesjh/rewriting-curry/issues",
"license": "BSD-3-Clause",
"licenseFile": "LICENSE.md",
"dependencies": {
"base" : ">= 3.0.0, < 4.0.0",
"abstract-curry": ">= 3.0.0, < 4.0.0",
"containers" : ">= 3.0.0, < 4.0.0",
"transformers" : ">= 3.0.0, < 4.0.0"
},
"compilerCompatibility": {
"pakcs": ">= 3.0.0, < 4.0.0",
"kics2": ">= 3.0.0, < 4.0.0"
},
"exportedModules": [
"Rewriting.CriticalPairs", "Rewriting.Narrowing", "Rewriting.Strategy",
"Rewriting.Unification", "Rewriting.DefinitionalTree",
......
......@@ -2,8 +2,7 @@
--- Library for representation and computation of critical pairs.
---
--- @author Jan-Hendrik Matthes
--- @version August 2016
--- @category algorithm
--- @version February 2020
------------------------------------------------------------------------------
module Rewriting.CriticalPairs
......@@ -48,15 +47,16 @@ showCPairs s = unlines . (map (showCPair s))
--- Returns the critical pairs of a term rewriting system.
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,
replaceTerm (applySubst sub l1) p (applySubst sub r2)) |
rule1@(l1, r1) <- trs',
p <- positions l1, let l1p = l1 |> p, isConsTerm l1p,
rule2@(l2, r2) <- trs,
(Right sub) <- [unify [(l1p, l2)]],
(p /= eps) || (not (isVariantOf rule1 rule2))]
cPairs trs =
let trs' = maybe trs (\v -> renameTRSVars (v + 1) trs) (maxVarInTRS trs)
in nub [(applySubst sub r1,
replaceTerm (applySubst sub l1) p (applySubst sub r2)) |
rule1@(l1, r1) <- trs',
p <- positions l1,
let l1p = l1 |> p, isConsTerm l1p,
rule2@(l2, r2) <- trs,
Right sub <- [unify [(l1p, l2)]],
p /= eps || not (rule1 `isVariantOf` rule2)]
-- ---------------------------------------------------------------------------
-- Functions for term rewriting systems and critical pairs
......@@ -64,8 +64,8 @@ cPairs trs
--- Checks whether a term rewriting system is orthogonal.
isOrthogonal :: Eq f => TRS f -> Bool
isOrthogonal trs = (isLeftLinear trs) && (null (cPairs trs))
isOrthogonal trs = isLeftLinear trs && null (cPairs trs)
--- Checks whether a term rewriting system is weak-orthogonal.
isWeakOrthogonal :: Eq f => TRS f -> Bool
isWeakOrthogonal trs = (isLeftLinear trs) && (all (uncurry (==)) (cPairs trs))
isWeakOrthogonal trs = isLeftLinear trs && all (uncurry (==)) (cPairs trs)
......@@ -3,8 +3,7 @@
--- representation of the reduction strategy phi.
---
--- @author Jan-Hendrik Matthes
--- @version August 2016
--- @category algorithm
--- @version February 2020
------------------------------------------------------------------------------
module Rewriting.DefinitionalTree
......@@ -16,7 +15,8 @@ module Rewriting.DefinitionalTree
import Data.Function (on)
import Data.Tuple.Extra (both)
import Data.List
import Data.Maybe (listToMaybe, catMaybes)
import Data.Maybe (listToMaybe, catMaybes, mapMaybe )
import Rewriting.Position (Pos, eps, positions, (.>), (|>), replaceTerm)
import Rewriting.Rules
import Rewriting.Strategy (RStrategy)
......@@ -65,28 +65,26 @@ 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 :: Eq f => [DefTree f] -> Term f -> [DefTree f]
selectDefTrees dts t = filter ((eqConsPattern t) . dtPattern) dts
selectDefTrees dts t = filter (eqConsPattern t . dtPattern) dts
--- Returns the definitional tree with the given index from the given list of
--- definitional trees or the provided default definitional tree if the given
--- index is not in the given list of definitional trees.
fromDefTrees :: DefTree f -> Int -> [DefTree f] -> DefTree f
fromDefTrees dt _ [] = dt
fromDefTrees dt n dts@(_:_) | (n >= 0) && (n < (length dts)) = dts !! n
| otherwise = dt
fromDefTrees dt _ [] = dt
fromDefTrees dt n dts@(_:_) | n >= 0 && n < length dts = dts !! n
| otherwise = dt
--- Returns a list of all inductive positions in a term rewriting system.
idtPositions :: TRS _ -> [Pos]
idtPositions [] = []
idtPositions trs@((l, _):_)
= case l of
(TermVar _) -> []
(TermCons _ ts) -> [[i] | i <- [1..(length ts)],
all (isDemandedAt i) trs]
idtPositions trs@((l, _):_) = case l of
TermVar _ -> []
TermCons _ ts -> [[i] | i <- [1 .. length ts], all (isDemandedAt i) trs]
--- Returns a list of definitional trees for a term rewriting system.
defTrees :: Eq f => TRS f -> [DefTree f]
defTrees = (concatMap defTreesS) . (groupBy eqCons) . (sortBy eqCons)
defTrees = concatMap defTreesS . groupBy eqCons . sortBy eqCons
where
eqCons = on eqConsPattern fst
......@@ -98,14 +96,12 @@ defTreesL = defTrees . concat
--- rules have the same constructor pattern.
defTreesS :: Eq f => TRS f -> [DefTree f]
defTreesS [] = []
defTreesS trs@((l, _):_)
= case l of
(TermVar _) -> []
(TermCons c ts) ->
let arity = length ts
pat = TermCons c (map TermVar [0..(arity - 1)])
pss = permutations (idtPositions trs)
in catMaybes [defTreesS' arity trs ps pat | ps <- pss]
defTreesS trs@((l, _):_) = case l of
TermVar _ -> []
TermCons c ts -> let arity = length ts
pat = TermCons c (map TermVar [0 .. arity - 1])
pss = permutations (idtPositions trs)
in catMaybes [defTreesS' arity trs ps pat | ps <- pss]
--- Returns a definitional tree for a term rewriting system, whose rules have
--- the same constructor pattern, with the given list of inductive positions,
......@@ -114,8 +110,8 @@ defTreesS trs@((l, _):_)
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
= mkOr v pat (partition (isDemandedAt 1) trs)
defTreesS' v trs@(_:_:_) [] pat =
mkOr v pat (partition (isDemandedAt 1) trs)
defTreesS' v trs (p:ps) pat = Just (Branch pat p dts)
where
nls = nub [normalizeTerm (l |> p) | (l, _) <- trs]
......@@ -132,39 +128,38 @@ defTreesS' v trs (p:ps) pat = Just (Branch pat p dts)
--- given next possible variable or `Nothing` if no such definitional tree
--- exists.
mkLeaf :: Eq f => VarIdx -> Term f -> Rule f -> Maybe (DefTree f)
mkLeaf v pat r
= case unify [(l, pat)] of
(Left _) -> Nothing
(Right sub)
| pat == (applySubst sub l) -> Just (Leaf (both (applySubst sub) r'))
| otherwise ->
let (ip:ips) = [p | p <- positions pat, isVarTerm (pat |> p)]
pat' = replaceTerm pat ip (l |> ip)
v' = max v (maybe 0 (+ 1) (maxVarInTerm pat'))
in Just (Branch pat ip (catMaybes [defTreesS' v' [r] ips pat']))
where
r'@(l, _) = renameRuleVars v (normalizeRule r)
mkLeaf v pat r = case unify [(l, pat)] of
Left _ -> Nothing
Right sub | pat == applySubst sub l -> Just (Leaf (both (applySubst sub) r'))
| otherwise ->
let (ip:ips) = [p | p <- positions pat, isVarTerm (pat |> p)]
pat' = replaceTerm pat ip (l |> ip)
v' = max v (maybe 0 (+ 1) (maxVarInTerm pat'))
in Just (Branch pat ip (catMaybes [defTreesS' v' [r] ips pat']))
where
r'@(l, _) = renameRuleVars v (normalizeRule r)
--- Returns a definitional tree for the given pattern, the given pair of term
--- 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 :: 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))
mkOr v pat (rs1@(_:_), [])
= defTreesS' v rs1 (intersect (idtPositions rs1) (varPositions pat)) pat
mkOr v pat (rs1@(_:_), rs2@(_:_))
= let vps = varPositions pat
mdts = [defTreesS' v rs (intersect (idtPositions rs) vps) pat |
rs <- [rs1, rs2]]
in Just (Or pat (catMaybes mdts))
mkOr _ _ ([], []) = Nothing
mkOr v pat ([], rs2@(_:_)) = Just (Or pat (mapMaybe (mkLeaf v pat) rs2))
mkOr v pat (rs1@(_:_), []) =
case intersect (idtPositions rs1) (varPositions pat) of
[] -> Just (Or pat (mapMaybe (mkLeaf v pat) rs1))
ps -> defTreesS' v rs1 ps pat
mkOr v pat (rs1@(_:_), rs2@(_:_)) =
let vps = varPositions pat
mdts = [defTreesS' v rs (intersect (idtPositions rs) vps) pat |
rs <- [rs1, rs2]]
in Just (Or pat (catMaybes mdts))
--- Returns a list of all variable argument positions in a term.
varPositions :: Term _ -> [Pos]
varPositions (TermVar _) = []
varPositions (TermCons _ ts) = [[i] | i <- [1..(length ts)],
varPositions (TermCons _ ts) = [[i] | i <- [1 .. length ts],
isVarTerm (ts !! (i - 1))]
-- ---------------------------------------------------------------------------
......@@ -187,15 +182,15 @@ 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 :: Eq f => Int -> RStrategy f
phiRStrategy n trs t
= let dts = defTrees trs
in case loDefTrees dts t of
Nothing -> []
(Just (_, [])) -> []
(Just (p, dts'@(dt:_))) ->
case phiRStrategy' n dts (t |> p) (fromDefTrees dt n dts') of
Nothing -> []
(Just p') -> [p .> p']
phiRStrategy n trs t =
let dts = defTrees trs
in case loDefTrees dts t of
Nothing -> []
Just (_, []) -> []
Just (p, dts'@(dt:_)) ->
case phiRStrategy' n dts (t |> p) (fromDefTrees dt n dts') of
Nothing -> []
Just p' -> [p .> p']
--- Returns the position for the reduction strategy phi where a term should be
--- reduced according to the given definitional tree or `Nothing` if no such
......@@ -208,18 +203,17 @@ phiRStrategy' _ _ t (Leaf (l, _))
where
l' = maybe l (\v -> renameTermVars (v + 1) l) (maxVarInTerm t)
phiRStrategy' _ _ (TermVar _) (Branch _ _ _) = Nothing
phiRStrategy' n dts t@(TermCons _ _) (Branch _ p dts')
= case t |> p of
(TermVar _) -> Nothing
tp@(TermCons _ _) ->
case selectDefTrees dts tp of
[] ->
case find (\dt -> eqConsPattern tp ((dtPattern dt) |> p)) dts' of
Nothing -> Nothing
(Just dt) -> phiRStrategy' n dts t dt
x@(dt:_) -> case phiRStrategy' n dts tp (fromDefTrees dt n x) of
Nothing -> Nothing
(Just p') -> Just (p .> p')
phiRStrategy' n dts t@(TermCons _ _) (Branch _ p dts') =
case t |> p of
TermVar _ -> Nothing
tp@(TermCons _ _) -> case selectDefTrees dts tp of
[] ->
case find (\dt -> eqConsPattern tp (dtPattern dt |> p)) dts' of
Nothing -> Nothing
Just dt -> phiRStrategy' n dts t dt
x@(dt:_) -> case phiRStrategy' n dts tp (fromDefTrees dt n x) of
Nothing -> Nothing
Just p' -> Just (p .> p')
phiRStrategy' _ _ _ (Or _ _) = Nothing
-- ---------------------------------------------------------------------------
......@@ -271,48 +265,47 @@ toGraph dt = fst (fst (runState (toGraph' dt) 0))
newIdx = modify (+1) >> get
--- Transforms a term into a string representation and surrounds the subterm
--- at the given position with the html `<u>` and `</u>` tags.
--- at the given position with the HTML `<u>` and `</u>` tags.
showTermWithPos :: (f -> String) -> (Maybe Pos, Term f) -> String
showTermWithPos s = showTP False
where
showTerm' _ (TermVar v) = showVarIdx v
showTerm' b (TermCons c ts)
= case ts of
[] -> s c
[l, r] -> parensIf b ((showTerm' True l) ++ " " ++ (s c) ++ " "
++ (showTerm' True r))
_ -> (s c) ++ "("
++ (intercalate "," (map (showTerm' False) ts)) ++ ")"
showTerm' b (TermCons c ts) = case ts of
[] -> s c
[l, r] -> parensIf b (showTerm' True l ++ " " ++ s c ++ " "
++ showTerm' True r)
_ -> s c ++ "(" ++ intercalate "," (map (showTerm' False) ts) ++ ")"
showTP b (Nothing, t) = showTerm' b t
showTP b (Just [], t) = "<u>" ++ (showTerm' b t) ++ "</u>"
showTP b (Just [], t) = "<u>" ++ showTerm' b t ++ "</u>"
showTP _ (Just (_:_), TermVar v) = showVarIdx v
showTP b (Just (p:ps), TermCons c ts)
= case [(mp, t) | (i, t) <- zip [1..] ts,
let mp = if i == p then (Just ps) else Nothing] of
[] -> s c
[l, r] -> parensIf b ((showTP True l) ++ " " ++ (s c) ++ " "
++ (showTP True r))
ts' -> (s c) ++ "(" ++ (intercalate "," (map (showTP False) ts'))
++ ")"
showTP b (Just (p:ps), TermCons c ts) =
case [(if i == p then Just ps else Nothing, t) |
(i, t) <- zip [1..] ts] of
[] -> s c
[l, r] -> parensIf b (showTP True l ++ " " ++ s c ++ " "
++ showTP True r)
ts' -> s c ++ "(" ++ intercalate "," (map (showTP False) ts') ++ ")"
--- Transforms a definitional tree into a graphical representation by using
--- the *DOT graph description language*.
dotifyDefTree :: (f -> String) -> DefTree f -> String
dotifyDefTree s dt = "digraph DefinitionalTree {\n\t"
++ "node [fontname=Helvetica,fontsize=10,shape=box];\n"
++ (unlines (map showNode ns))
++ "\tedge [arrowhead=none];\n"
++ (unlines (map showEdge es)) ++ "}"
dotifyDefTree s dt = "digraph definitional_tree {\n"
++ " graph [margin=0.0];\n"
++ " node [fontname=\"Menlo\",fontsize=10.0,shape=box];\n"
++ unlines (map showNode ns)
++ " edge [fontname=\"Menlo\",fontsize=7.0,arrowhead=none];\n"
++ unlines (map showEdge es)
++ "}"
where
(ns, es) = toGraph dt
showNode (n, p, t) = "\t" ++ (showVarIdx n) ++ " [label=<"
++ (showTermWithPos s (p, t)) ++ ">];"
showNode (n, p, t) =
" " ++ showVarIdx n ++ " [label=<" ++ showTermWithPos s (p, t) ++ ">];"
showEdge (b, (n1, _, _), (n2, _, _))
= let opts = if b then " [arrowhead=normal];" else ";"
in "\t" ++ (showVarIdx n1) ++ " -> " ++ (showVarIdx n2) ++ opts
showEdge (b, (n1, _, _), (n2, _, _)) =
let opts = if b then " [arrowhead=normal];" else ";"
in " " ++ showVarIdx n1 ++ " -> " ++ showVarIdx n2 ++ opts
--- Writes the graphical representation of a definitional tree with the
--- *DOT graph description language* to a file with the given filename.
......
------------------------------------------------------------------------------
--- Library to read and transform a curry program into an equivalent
--- Library to read and transform a Curry program into an equivalent
--- representation, where every function gets assigned the corresponding term
--- rewriting system and every type has a corresponding type declaration.
---
--- @author Jan-Hendrik Matthes
--- @version October 2016
--- @category algorithm
--- @version February 2020
------------------------------------------------------------------------------
module Rewriting.Files
......@@ -52,7 +51,7 @@ readQName s = case break (== '.') s of
(mn, _:fn) -> (mn, fn)
-- ---------------------------------------------------------------------------
-- Functions for transforming (abstract) curry programs
-- Functions for transforming (abstract) Curry programs
-- ---------------------------------------------------------------------------
--- Returns the qualified name for an `if-then-else`-constructor.
......@@ -66,95 +65,94 @@ condTRS = let tTrue = tConst (pre "True")
in [(TermCons condQName [tTrue, TermVar 0, TermVar 1], TermVar 0),
(TermCons condQName [tFalse, TermVar 0, TermVar 1], TermVar 1)]
--- Tries to read and transform a curry program into an equivalent
--- Tries to read and transform a Curry program into an equivalent
--- representation, where every function gets assigned the corresponding term
--- rewriting system and every type has a corresponding type declaration.
readCurryProgram :: String -> IO (Either String RWData)
readCurryProgram fn = do res <- tryReadCurryFile fn
case res of
(Left e) -> return (Left e)
(Right cp) -> return (Right (fromCurryProg cp))
Left e -> return (Left e)
Right cp -> return (Right (fromCurryProg cp))
--- Transforms an abstract curry program into an equivalent representation,
--- Transforms an abstract Curry program into an equivalent representation,
--- 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 _)
= (Map.fromList (map fromFuncDecl fs), ts)
--- Transforms an abstract curry function declaration into a pair with
--- Transforms an abstract Curry function declaration into a pair with
--- function name and corresponding term rewriting system.
fromFuncDecl :: CFuncDecl -> (QName, TRS QName)
fromFuncDecl (CFunc fn _ _ _ rs)
= let (trs, trss) = unzip (map (fromRule fn) rs)
cond = if elem condQName (concatMap rCons trs) then condTRS else []
in (fn, trs ++ (concat trss) ++ cond)
fromFuncDecl (CFunc fn _ _ _ rs) =
let (trs, trss) = unzip (map (fromRule fn) rs)
cond = if elem condQName (concatMap rCons trs) then condTRS else []
in (fn, trs ++ concat trss ++ cond)
fromFuncDecl (CmtFunc _ fn a v t rs) = fromFuncDecl (CFunc fn a v t rs)
--- Transforms an abstract curry rule for the function with the given name
--- into a pair of a rule and a term rewriting system.
fromRule :: QName -> CRule -> (Rule QName, TRS QName)
fromRule fn (CRule ps rhs)
= let (ts, subs) = unzip (map (fromPattern fn) ps)
(r, sub, trs) = fromRhs fn rhs
sub' = foldr composeSubst emptySubst (sub:subs)
in ((TermCons fn ts, applySubst sub' r), trs)
fromRule fn (CRule ps rhs) = let (ts, subs) = unzip (map (fromPattern fn) ps)
(r, sub, trs) = fromRhs fn rhs
sub' = foldr composeSubst emptySubst (sub:subs)
in ((TermCons fn ts, applySubst sub' r), trs)
--- Transforms an abstract curry literal into a term.
--- Transforms an abstract Curry literal into a term.
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)
--- Transforms an abstract curry pattern for the function with the given name
--- Transforms an abstract Curry pattern for the function with the given name
--- into a pair of a term and a substitution.
fromPattern :: QName -> CPattern -> (Term QName, Subst QName)
fromPattern _ (CPVar (v, _)) = (TermVar v, emptySubst)
fromPattern _ (CPLit l) = (fromLiteral l, emptySubst)
fromPattern fn (CPComb c ps)
= let (ts, subs) = unzip (map (fromPattern fn) ps)
in (TermCons c ts, foldr composeSubst emptySubst subs)
fromPattern fn (CPComb c ps) =
let (ts, subs) = unzip (map (fromPattern fn) ps)
in (TermCons c ts, foldr composeSubst emptySubst subs)
fromPattern fn (CPAs (v, _) p) = let (t, sub) = fromPattern fn p
in (t, extendSubst sub v t)
fromPattern fn (CPFuncComb c ps)
= let (ts, subs) = unzip (map (fromPattern fn) ps)
in (TermCons c ts, foldr composeSubst emptySubst subs)
fromPattern fn (CPFuncComb c ps) =
let (ts, subs) = unzip (map (fromPattern fn) ps)
in (TermCons c ts, foldr composeSubst emptySubst subs)
fromPattern fn (CPLazy p) = fromPattern fn p
fromPattern fn (CPRecord _ _) = error (pError "fromPattern" "CPRecord" fn)
--- Transforms an abstract curry right-hand side of a rule for the function
--- with the given name into a tuple of a term, a substitution and a term
--- rewriting system.
--- Transforms an abstract Curry right-hand side of a rule for the function with
--- the given name into a tuple of a term, a substitution and a term rewriting
--- system.
fromRhs :: QName -> CRhs -> (Term QName, Subst QName, TRS QName)
fromRhs fn (CSimpleRhs e _) = fromExpr fn e
fromRhs fn (CGuardedRhs gs _) = fromGuard fn gs
--- Transforms a list of abstract curry guarded expressions for the function
--- Transforms a list of abstract Curry guarded expressions for the function
--- with the given name into a tuple of a term, a substitution and a term
--- rewriting system.
fromGuard :: QName -> [(CExpr, CExpr)] -> (Term QName, Subst QName, TRS QName)
fromGuard _ [] = (tConst (pre "failed"), emptySubst, [])
fromGuard fn ((c, e):gs)
= let (ct, cs, ctrs) = fromExpr fn c
(et, es, etrs) = fromExpr fn e
(gt, gsub, gtrs) = fromGuard fn gs
sub = composeSubst cs (composeSubst es gsub)
in (TermCons condQName [ct, et, gt], sub, ctrs ++ etrs ++ gtrs)
--- Transforms an abstract curry expression for the function with the given
fromGuard fn ((c, e):gs) =
let (ct, cs, ctrs) = fromExpr fn c
(et, es, etrs) = fromExpr fn e
(gt, gsub, gtrs) = fromGuard fn gs
sub = composeSubst cs (composeSubst es gsub)
in (TermCons condQName [ct, et, gt], sub, ctrs ++ etrs ++ gtrs)
--- Transforms an abstract Curry expression for the function with the given
--- name into a tuple of a term, a substitution and a term rewriting system.
fromExpr :: QName -> CExpr -> (Term QName, Subst QName, TRS QName)
fromExpr _ (CVar (v, _)) = (TermVar v, emptySubst, [])
fromExpr _ (CLit l) = (fromLiteral l, emptySubst, [])
fromExpr _ (CSymbol s) = (tConst s, emptySubst, [])
fromExpr fn (CApply fe e)
= let (ft, fs, ftrs) = fromExpr fn fe
(et, es, etrs) = fromExpr fn e
sub = composeSubst fs es
in case ft of
(TermVar _) -> error "fromExpr: Argument is not a function!"
(TermCons c ts) -> (TermCons c (ts ++ [et]), sub, ftrs ++ etrs)
fromExpr fn (CApply fe e) =
let (ft, fs, ftrs) = fromExpr fn fe
(et, es, etrs) = fromExpr fn e
sub = composeSubst fs es
in case ft of
TermVar _ -> error "fromExpr: Argument is not a function!"
TermCons c ts -> (TermCons c (ts ++ [et]), sub, ftrs ++ etrs)
fromExpr fn (CLambda _ _) = error (pError "fromExpr" "CLambda" fn)
fromExpr fn (CLetDecl _ _) = error (pError "fromExpr" "CLetDecl" fn)
fromExpr fn (CDoExpr _) = error (pError "fromExpr" "CDoExpr" fn)
......@@ -168,12 +166,12 @@ fromExpr fn (CRecUpdate _ _) = error (pError "fromExpr" "CRecUpdate" fn)
-- Definition of helper functions
-- ---------------------------------------------------------------------------
--- Error message for the given function and the feature, that is not
--- supported within the given abstract curry function.
--- Returns an error message for the given function and the feature, that is not
--- supported within the given abstract Curry function.
pError :: String -> String -> QName -> String
pError fn f acf
= let fn' = if null fn then "" else fn ++ ": "
f' = if null f then "Feature" else f
in case showQName acf of
[] -> fn' ++ f' ++ " currently not supported!"
x@(_:_) -> fn' ++ f' ++ " in " ++ x ++ " currently not supported!"
pError fn f acf =
let fn' = if null fn then "" else fn ++ ": "
f' = if null f then "Feature" else f
in case showQName acf of
[] -> fn' ++ f' ++ " currently not supported!"
x@(_:_) -> fn' ++ f' ++ " in " ++ x ++ " currently not supported!"
......@@ -85,10 +85,10 @@ defaultNOptions = NOptions { normalize = False, rStrategy = poRStrategy }
--- Transforms a narrowing into a string representation.
showNarrowing :: (f -> String) -> Narrowing f -> String
showNarrowing s (NTerm t) = showTerm s t
showNarrowing s (NStep t p sub n)
= (showTerm s t) ++ "\n\x2192" ++ "[" ++ (showPos p) ++ ", "
++ (showSubst s (restrictSubst sub (tVars t))) ++ "] "
++ (showNarrowing s n)
showNarrowing s (NStep t p sub n) =
showTerm s t ++ "\n\x2192" ++ "[" ++ showPos p ++ ", "
++ showSubst s (restrictSubst sub (tVars t)) ++ "] "
++ showNarrowing s n
-- ---------------------------------------------------------------------------
-- Definition of common narrowing strategies
......@@ -96,17 +96,17 @@ showNarrowing s (NStep t p sub n)
--- The standard narrowing strategy.
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)]]]
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 :: 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)]]]
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 :: Eq f => NStrategy f
......@@ -117,17 +117,16 @@ omNStrategy trs t = let ns = stdNStrategy trs t
--- The leftmost outermost narrowing strategy.
loNStrategy :: Eq f => NStrategy f
loNStrategy trs t
= let ns = stdNStrategy trs t
in [n | n@(p, _, _) <- ns,
all (\p' -> not ((above p' p) || (leftOf p' p)))
[p' | (p', _, _) <- ns, p' /= p]]
loNStrategy trs t =
let ns = stdNStrategy trs t
in [n | n@(p, _, _) <- ns,
all (\p' -> not (above p' p || leftOf p' p))
[p' | (p', _, _) <- ns, p' /= p]]
--- The lazy narrowing strategy.
lazyNStrategy :: Eq f => NStrategy f
lazyNStrategy trs t
= let lps = lazyPositions trs t
in filter (\(p, _, _) -> elem p lps) (stdNStrategy trs t)
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.
......@@ -137,41 +136,41 @@ lazyPositions trs t@(TermCons _ ts)
| isRedex trs t = if null rs then lps else eps:lps
| otherwise = [i:p | (i, t') <- zip [1..] ts, p <- lazyPositions trs t']
where
ftrs = filter ((eqConsPattern t) . fst) trs
ftrs = filter (eqConsPattern t . fst) trs
rs = [r | r@(l, _) <- ftrs, unifiable [(t, l)]]
dps = [i | (i, _) <- zip [1..] ts, any (isDemandedAt i) ftrs]
lps = [i:p | i <- dps, p <- lazyPositions trs (ts !! (i - 1))]
--- The weakly needed narrowing strategy.
wnNStrategy :: Eq f => NStrategy f
wnNStrategy trs t