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
2e354ddd
Commit
2e354ddd
authored
Mar 29, 2017
by
Michael Hanus
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Rewriting libraries from PAKCS/KiCS2 lib-trunk packaged
parents
Changes
13
Hide whitespace changes
Inline
Side-by-side
Showing
13 changed files
with
2081 additions
and
0 deletions
+2081
-0
.gitignore
.gitignore
+3
-0
package.json
package.json
+25
-0
src/Rewriting/CriticalPairs.curry
src/Rewriting/CriticalPairs.curry
+72
-0
src/Rewriting/DefinitionalTree.curry
src/Rewriting/DefinitionalTree.curry
+331
-0
src/Rewriting/Files.curry
src/Rewriting/Files.curry
+180
-0
src/Rewriting/Narrowing.curry
src/Rewriting/Narrowing.curry
+395
-0
src/Rewriting/Position.curry
src/Rewriting/Position.curry
+103
-0
src/Rewriting/Rules.curry
src/Rewriting/Rules.curry
+145
-0
src/Rewriting/Strategy.curry
src/Rewriting/Strategy.curry
+230
-0
src/Rewriting/Substitution.curry
src/Rewriting/Substitution.curry
+97
-0
src/Rewriting/Term.curry
src/Rewriting/Term.curry
+199
-0
src/Rewriting/Unification.curry
src/Rewriting/Unification.curry
+179
-0
src/Rewriting/UnificationSpec.curry
src/Rewriting/UnificationSpec.curry
+122
-0
No files found.
.gitignore
0 → 100644
View file @
2e354ddd
*~
.cpm
.curry
package.json
0 → 100644
View file @
2e354ddd
{
"name"
:
"rewriting"
,
"version"
:
"0.0.1"
,
"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"
,
"description"
:
"These libraries provide 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
PAKCS/KiCS2 distributions."
,
"category"
:
[
"Rewriting"
,
"Narrowing"
],
"dependencies"
:
{
},
"exportedModules"
:
[
"Rewriting.CriticalPairs"
,
"Rewriting.Narrowing"
,
"Rewriting.Strategy"
,
"Rewriting.Unification"
,
"Rewriting.DefinitionalTree"
,
"Rewriting.Position"
,
"Rewriting.Substitution"
,
"Rewriting.UnificationSpec"
,
"Rewriting.Files"
,
"Rewriting.Rules"
,
"Rewriting.Term"
]
}
src/Rewriting/CriticalPairs.curry
0 → 100644
View file @
2e354ddd
------------------------------------------------------------------------------
--- Library for representation and computation of critical pairs.
---
--- @author Jan-Hendrik Matthes
--- @version August 2016
--- @category algorithm
------------------------------------------------------------------------------
module Rewriting.CriticalPairs
( CPair
, showCPair, showCPairs, cPairs, isOrthogonal, isWeakOrthogonal
) where
import List (nub)
import Rewriting.Position (eps, positions, (|>), replaceTerm)
import Rewriting.Rules
import Rewriting.Substitution (applySubst)
import Rewriting.Term (Term, showTerm, isConsTerm)
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"
--- Transforms a list of critical pairs into a string representation.
showCPairs :: (f -> String) -> [CPair f] -> String
showCPairs s = unlines . (map (showCPair s))
-- ---------------------------------------------------------------------------
-- Computation of critical pairs
-- ---------------------------------------------------------------------------
--- Returns the critical pairs of a term rewriting system.
cPairs :: 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))]
-- ---------------------------------------------------------------------------
-- Functions for term rewriting systems and critical pairs
-- ---------------------------------------------------------------------------
--- Checks whether a term rewriting system is orthogonal.
isOrthogonal :: TRS _ -> Bool
isOrthogonal trs = (isLeftLinear trs) && (null (cPairs trs))
--- Checks whether a term rewriting system is weak-orthogonal.
isWeakOrthogonal :: TRS _ -> Bool
isWeakOrthogonal trs = (isLeftLinear trs) && (all (uncurry (==)) (cPairs trs))
\ No newline at end of file
src/Rewriting/DefinitionalTree.curry
0 → 100644
View file @
2e354ddd
------------------------------------------------------------------------------
--- Library for representation and computation of definitional trees and
--- representation of the reduction strategy phi.
---
--- @author Jan-Hendrik Matthes
--- @version August 2016
--- @category algorithm
------------------------------------------------------------------------------
module Rewriting.DefinitionalTree
( DefTree (..)
, dtRoot, dtPattern, hasDefTree, selectDefTrees, fromDefTrees, idtPositions
, defTrees, defTreesL, loDefTrees, phiRStrategy, dotifyDefTree, writeDefTree
) where
import Function (on, both)
import List
import Maybe (listToMaybe, catMaybes)
import Rewriting.Position (Pos, eps, positions, (.>), (|>), replaceTerm)
import Rewriting.Rules
import Rewriting.Strategy (RStrategy)
import Rewriting.Substitution (applySubst)
import Rewriting.Term
import Rewriting.Unification (unify, unifiable)
import State
-- ---------------------------------------------------------------------------
-- Representation of definitional trees
-- ---------------------------------------------------------------------------
--- Representation of a definitional tree, parameterized over the kind of
--- function symbols, e.g., strings.
---
--- @cons Leaf r - The leaf with rule `r`.
--- @cons Branch pat p dts - The branch with pattern `pat`, inductive position
--- `p` and definitional subtrees `dts`.
--- @cons Or pat dts - The or node with pattern `pat` and definitional
--- subtrees `dts`.
data DefTree f = Leaf (Rule f)
| Branch (Term f) Pos [DefTree f]
| Or (Term f) [DefTree f]
-- ---------------------------------------------------------------------------
-- Functions for definitional trees
-- ---------------------------------------------------------------------------
--- Returns the root symbol (variable or constructor) of a definitional tree.
dtRoot :: DefTree f -> Either VarIdx f
dtRoot (Leaf r) = rRoot r
dtRoot (Branch pat _ _) = tRoot pat
dtRoot (Or pat _) = tRoot pat
--- Returns the pattern of a definitional tree.
dtPattern :: DefTree f -> Term f
dtPattern (Leaf (l, _)) = l
dtPattern (Branch pat _ _) = pat
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 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 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
--- 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]
--- Returns a list of definitional trees for a term rewriting system.
defTrees :: 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 = 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 [] = []
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,
--- 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' _ [] [] _ = Nothing
defTreesS' v [r] [] pat = mkLeaf v pat r
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]
ts = map (renameTermVars v) nls
pats = [replaceTerm pat p t | t <- ts]
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 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 :: 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))
--- Returns a list of all variable argument positions in a term.
varPositions :: Term _ -> [Pos]
varPositions (TermVar _) = []
varPositions (TermCons _ ts) = [[i] | i <- [1..(length ts)],
isVarTerm (ts !! (i - 1))]
-- ---------------------------------------------------------------------------
-- Functions for the reduction strategy phi
-- ---------------------------------------------------------------------------
--- 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 [] _ = 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)]
| otherwise = [lp | (p', t') <- zip [1..] ts,
lp <- loDefTrees' (p .> [p']) 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 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
--- 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' _ _ t (Leaf (l, _))
| unifiable [(l', t)] = Just eps
| otherwise = Nothing
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' _ _ _ (Or _ _) = Nothing
-- ---------------------------------------------------------------------------
-- Graphical representation of definitional trees
-- ---------------------------------------------------------------------------
--- A node represented as a tuple of an integer, a possible inductive position
--- and a term and parameterized over the kind of function symbols, e.g.,
--- strings.
type Node f = (Int, Maybe Pos, Term f)
--- An edge represented as a tuple of a boolean to distinguish between branch
--- (`False`) and rule (`True`) edges, a start node and an end node and
--- parameterized over the kind of function symbols, e.g., strings.
type Edge f = (Bool, Node f, Node f)
--- A graph represented as a tuple of nodes and edges and parameterized over
--- the kind of function symbols, e.g., strings.
type Graph f = ([Node f], [Edge f])
--- Transforms a definitional tree into a graph representation.
toGraph :: DefTree f -> Graph f
toGraph dt = fst (fst (runState (toGraph' dt) 0))
where
toGraph' :: DefTree f -> State Int (Graph f, Node f)
toGraph' (Leaf (l, r))
= newIdx `bindS`
(\i -> let n = (i, Nothing, l)
in (mapS (ruleEdge n) [r]) `bindS` (addNode n))
toGraph' (Branch pat p dts)
= newIdx `bindS`
(\i -> let n = (i, Just p, pat)
in (mapS (branchEdge n) dts) `bindS` (addNode n))
toGraph' (Or pat dts)
= newIdx `bindS`
(\i -> let n = (i, Nothing, pat)
in (mapS (branchEdge n) dts) `bindS` (addNode n))
addNode :: Node f -> [Graph f] -> State Int (Graph f, Node f)
addNode n gs = let (ns, es) = unzip gs
in returnS ((n:(concat ns), concat es), n)
branchEdge :: Node f -> DefTree f -> State Int (Graph f)
branchEdge n1 dt'
= (toGraph' dt') `bindS`
(\((ns, es), n2) -> returnS (ns, (False, n1, n2):es))
ruleEdge :: Node f -> Term f -> State Int (Graph f)
ruleEdge n1 t = newIdx `bindS` (\i -> let n = (i, Nothing, t)
in returnS ([n], [(True, n1, n)]))
newIdx :: State Int Int
newIdx = getS `bindS` (\i -> (putS (i + 1)) `bindS_` (returnS i))
--- Transforms a term into a string representation and surrounds the subterm
--- 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' :: Bool -> Term f -> String
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)) ++ ")"
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
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'))
++ ")"
--- 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)) ++ "}"
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
--- Writes the graphical representation of a definitional tree with the
--- *DOT graph description language* to a file with the given filename.
writeDefTree :: (f -> String) -> DefTree f -> String -> IO ()
writeDefTree s dt fn = writeFile fn (dotifyDefTree s dt)
-- ---------------------------------------------------------------------------
-- Definition of helper functions
-- ---------------------------------------------------------------------------
--- Encloses a string in parenthesis if the given condition is true.
parensIf :: Bool -> String -> String
parensIf b s = if b then "(" ++ s ++ ")" else s
\ No newline at end of file
src/Rewriting/Files.curry
0 → 100644
View file @
2e354ddd
------------------------------------------------------------------------------
--- 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 August 2016
--- @category algorithm
------------------------------------------------------------------------------
module Rewriting.Files
( TRSData, TypeData, RWData
, showQName, readQName, condQName, condTRS, readCurryProgram, fromCurryProg
, fromFuncDecl, fromRule, fromLiteral, fromPattern, fromRhs, fromExpr
) where
import AbstractCurry.Files (tryReadCurryFile)
import AbstractCurry.Types
import FiniteMap (FM, listToFM)
import Rewriting.Rules (Rule, TRS, rCons)
import Rewriting.Substitution
import Rewriting.Term (Term (..), tConst)
-- ---------------------------------------------------------------------------
-- Representation of term rewriting system data and type data
-- ---------------------------------------------------------------------------
--- Mappings from a function name to the corresponding term rewriting system
--- represented as a finite map from qualified names to term rewriting
--- systems.
type TRSData = FM QName (TRS QName)
--- Information about types represented as a list of type declarations.
type TypeData = [CTypeDecl]
--- Representation of term rewriting system data and type data as a pair.
type RWData = (TRSData, TypeData)
-- ---------------------------------------------------------------------------
-- Pretty-printing and reading of qualified names
-- ---------------------------------------------------------------------------
--- Transforms a qualified name into a string representation.
showQName :: QName -> String
showQName (mn, fn) | null mn = fn
| otherwise = mn ++ "." ++ fn
--- Transforms a string into a qualified name.
readQName :: String -> QName
readQName s = case break (== '.') s of
qn@(_, []) -> qn
(mn, _:fn) -> (mn, fn)
-- ---------------------------------------------------------------------------
-- Functions for transforming (abstract) curry programs
-- ---------------------------------------------------------------------------
--- Returns the qualified name for an `if-then-else`-constructor.
condQName :: QName
condQName = pre "_if_"
--- Returns the term rewriting system for an `if-then-else`-function.
condTRS :: TRS QName
condTRS = let tTrue = tConst (pre "True")
tFalse = tConst (pre "False")
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
--- 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))
--- 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 _)
= (listToFM (<) (map fromFuncDecl fs), ts)
--- 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 (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)
--- 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
--- 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 (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 (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.
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
--- 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
--- 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 (CLambda _ _) = error (pError "fromExpr" "CLambda" fn)
fromExpr fn (CLetDecl _ _) = error (pError "fromExpr" "CLetDecl" fn)
fromExpr fn (CDoExpr _) = error (pError "fromExpr" "CDoExpr" fn)
fromExpr fn (CListComp _ _) = error (pError "fromExpr" "CListComp" fn)
fromExpr fn (CCase _ _ _) = error (pError "fromExpr" "CCase" fn)
fromExpr fn (CTyped e _) = fromExpr fn e
fromExpr fn (CRecConstr _ _) = error (pError "fromExpr" "CRecConstr" fn)
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.
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!"
\ No newline at end of file
src/Rewriting/Narrowing.curry
0 → 100644
View file @
2e354ddd
------------------------------------------------------------------------------
--- Library for representation and computation of narrowings on first-order
--- terms and representation of narrowing strategies.
---
--- @author Jan-Hendrik Matthes
--- @version November 2016
--- @category algorithm
------------------------------------------------------------------------------
module Rewriting.Narrowing
( NStrategy, Narrowing (..), NarrowingTree (..), NOptions (..)
, defaultNOptions, showNarrowing, stdNStrategy, imNStrategy, omNStrategy
, loNStrategy, lazyNStrategy, wnNStrategy, narrowBy, narrowByL, narrowingBy
, narrowingByL, narrowingTreeBy, narrowingTreeByL, solveEq, solveEqL
, dotifyNarrowingTree, writeNarrowingTree
) where
import FiniteMap (eltsFM)
import Maybe (fromMaybe, mapMaybe)
import List (maximum)
import Rewriting.DefinitionalTree
import Rewriting.Position
import Rewriting.Rules
import Rewriting.Strategy (RStrategy, poRStrategy, reduce)